# Formal, Executable and Explainable Runtime Monitoring of Spoken Air Traffic Control Operational Procedures

arXiv: https://arxiv.org/abs/2608.25926 · HTML: https://mlsanity.com/paper/2608.25926/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 7 of its 41 references that are in the map.
- First posted on arXiv 26 Aug 2026.

## Builds on (most cited first, 7 of 7)

- [Qwen2.5 Technical Report](https://mlsanity.com/paper/2412.15115/) (2024)
- [Robust Speech Recognition via Large-Scale Weak Supervision](https://mlsanity.com/paper/2212.04356/) (2022)
- [Open ASR Leaderboard: Towards Reproducible and Transparent Multilingual and Long-Form Speech Recognition Evaluation](https://mlsanity.com/paper/2510.06961/) (2025)
- [ATCO2 corpus: A Large-Scale Dataset for Research on Automatic Speech Recognition and Natural Language Understanding of Air Traffic Control Communications](https://mlsanity.com/paper/2211.04054/) (2022)
- [TartanAviation: Image, Speech, and ADS-B Trajectory Datasets for Terminal Airspace Operations](https://mlsanity.com/paper/2403.03372/) (2024)
- [A Virtual Simulation-Pilot Agent for Training of Air Traffic Controllers](https://mlsanity.com/paper/2304.07842/) (2023)
- [Prompt-and-Check: Using Large Language Models to Evaluate Communication Protocol Compliance in Simulation-Based Training](https://mlsanity.com/paper/2508.08652/) (2025)

## Abstract (arXiv)

Air traffic control procedures are executed through spoken exchanges between controllers and pilots. These interactions are essential to the safety of air transportation: failures in their execution can create severe operational hazards, as evidenced by past fatal accidents. Assessing whether an instruction has been followed requires relating what was said to the aircraft concerned, its state, and the obligations that pilots must meet. We present a runtime verification framework that monitors such procedures by checking controller-pilot exchanges, surveillance data, and onboard observations. The framework parses radio communications into events linked to the entities they concern and merges them with surveillance and onboard observations into a time-stamped trace. The ICAO-derived obligations as formalized as temporal formulas with explicit time bounds and evaluated over execution traces. Every violation is reported along with the breached obligations and the observations that support the verdict. With real traffic, the complete pipeline reaches an F1 of 0.85 against blind human-annotated violations; in 1,495 synthetic situations derived from two public corpora, the monitor logic returns the expected verdict in every case. In two historical accidents reconstructed from official investigation reports, the monitor identifies the same procedural deviations documented by the investigators.