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

arXiv:2608.25926v1 Announce Type: cross Abstract: 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.

Related

• Safety-Oriented Evaluation of Language Understanding Systems for Air Traffic Control
• Safety Verification of Wait-Only Non-Blocking Broadcast Protocols
• Generation-Step-Aware Framework for Cross-Modal Representation and Control in Multilingual Speech-Text Models

Source: arXiv cs.CL | 2026-08-27