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

Roberto Luvini; Giacomo Longo; Alessandro Armando; Enrico Russo

cs.AIAug 26, 2026

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

Authors: Roberto Luvini, Giacomo Longo, Alessandro Armando, Enrico Russo

Organizations: Department of Informatics, Bioengineering, Robotics, and Systems Engineering (DIBRIS), University of Genoa, Italy · CASD - University School of Advanced Defense Studies, Rome, Italy

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.

Figures & tables

Family	Pattern	$\boldsymbol{\alpha}$	$\boldsymbol{\beta}$	Source
readback	bounded-response $\mathbf{G}(\alpha\rightarrow\mathbf{F}_{\leq\delta}\beta)$	$\mathit{Says}(\text{\scriptsize{atc}},\allowbreak\ \text{\scriptsize{cmd\_descend}}(a,\ell))$	$\mathit{Says}(\text{\scriptsize{pilot}},\allowbreak\ \text{\scriptsize{readback\_descend}}(a,\ell))$	[ 18 , §4.5.7.5] [ 17 , §5.2.1.9.2.1]
state-consistency		$\mathit{Says}(\text{\scriptsize{pilot}},\allowbreak\ \text{\scriptsize{readback\_descend}}(a,\ell))$	$\text{\scriptsize{descending}}(a)$	[ 18 , §4.5.7.5.1.1]
RA		$\text{\scriptsize{ra\_climb}}(a)$	$\text{\scriptsize{climbing}}(a)$	[ 15 , §4.1.4.2]
runway-incursion	invariant $\mathbf{G}(\alpha\rightarrow\beta)$	$\text{\scriptsize{on\_runway}}(a,r)$	$\text{\scriptsize{line\_up\_authorized}}(a,r)$	[ 18 , §7.6.3.1.1.2] [ 18 , §7.6.3.1.2.1]
advisory-priority		$\text{\scriptsize{ra\_active}}(a)$	$\neg\,\mathit{Says}(\text{\scriptsize{atc}},\allowbreak\ \text{\scriptsize{cmd\_descend}}(a,\ell))$	[ 18 , §15.7.3.2]
clearance-precedence	precedence $\neg\,\alpha\ \mathbf{W}\ \beta$	$\text{\scriptsize{landed}}(a)$	$\text{\scriptsize{landing\_cleared}}(a)$	[ 18 , §7.10.2] [ 18 , §6.5.6]

TABLE I: Families with pattern, formula, representative forms of

\alpha

and

\beta

, and source.

Fig. 1: Framework architecture and workflow.

Parser	Precision	Recall	F1
qwen3.8-27b , no-thinking (NT)	0.79	0.92	0.85
qwen3.8-27b , thinking (T)	0.78	0.58	0.67
gemma4-26b-a4b , no-thinking (NT)	0.40	0.33	0.36
gemma4-26b-a4b , thinking (T)	0.67	0.33	0.44
qwen2.5-7b , no-thinking	0.57	0.67	0.62

TABLE II: Performance by parser model

Stage	Min	$\textbf{Q}_{1}$	Median	$\textbf{Q}_{3}$	Max	Unit
Speech recognition	32.1	41.4	45.1	47.5	48.7	RTFx
Atom parse (Small LLM)	0.266	0.282	0.296	0.339	1.46	s/utt.
Atom parse (Large LLM)	1.16	1.34	1.58	1.75	4.94	s/utt.
Formula evaluation	0.000003	0.037	0.119	0.245	2.54	s/event

TABLE III: Per-stage processing cost.

Panel of Figure 5 — Fig. 2: Per-utterance parse latency.

Panel of Figure 6 — Fig. 3: Accuracy versus parse latency.

Panel of Figure 7 — Fig. 4: Überlingen: monitor detections and BFU-documented events (UTC).

Panel of Figure 8 — Fig. 5: Comair: monitor detections and NTSB-documented events (EDT).

Panel of Table 9 — TABLE IV: Requirement coverage: related work vs. this work.

Explore similar work

SCOPE: A Lightweight-training LLM Framework for Air Traffic Control Readback Monitoring
May 28, 2026Qihan Deng, Minghua Zhang, Yang Yang +1Air Traffic Management Intelligent Transportation Systems
Department of Mechanical and Aerospace Engineering, The Hong Kong University of Science and Technology, Clear Water Bay, 999077, Hong Kong · School of Electronic and Information Engineering, Beihang University, Beijing, 100191, China · State Key Laboratory of CNS/ATM, Beijing, 100191, China
Safety-Oriented Evaluation of Language Understanding Systems for Air Traffic Control
May 12, 2026Yujing Chang, Yash Guleria, Duc-Thinh Pham +4LLM Grounding Air Traffic Management
1ATMRI, Nanyang Technological University (NTU), Singapore · School of Management, Indian Institute of Technology Mandi, India · Centre of AI Research, VinUniversity, Vietnam
AeroCopilotBench: Safety-Gated Evaluation of LLM Agents on Aircraft Emergency Procedures in an Executable Cockpit
Aug 17, 2026Yuchen Yuan, Zhenghuang Wu, Yuangan Li +2LLM Safety Benchmarks AI Agent Safety Benchmarks
School of Aeronautic Science and Engineering, Beihang University

May 28, 2026J/K move · Enter open · S save

SCOPE: A Lightweight-training LLM Framework for Air Traffic Control Readback Monitoring

Qihan Deng, Minghua Zhang, Yang Yang, Zhenyu Gao

Department of Mechanical and Aerospace Engineering, The Hong Kong University of Science and Technology, Clear Water Bay, 999077, Hong Kong · School of Electronic and Information Engineering, Beihang University, Beijing, 100191, China · State Key Laboratory of CNS/ATM, Beijing, 100191, China

Air Traffic Management Intelligent Transportation Systems

Open paper AskPDF arXiv

Pilot readback of Air Traffic Control (ATC) voice instructions is a primary safeguard against miscommunication in air transportation. However, readback anomalies remain implicated in approximately 80% of aviation incidents. This vulnerability is further exacerbated by rising traffic volume and elevated cognitive workload, thereby motivating automated readback monitoring by machine. Traditional rule-based and machine learning approaches struggle to generalize across the highly variable and evolving phraseology of air traffic controller-pilot communications. While Large Language Models (LLMs) have opened a new avenue through their strong reasoning and generalization capabilities, existing approaches still face deployment and computational barriers in practice. In this work, we propose Semantic reasoning for Communication via Open-set Plug-in with Examples (SCOPE), a novel lightweight-training LLM framework that advances both the efficiency and accuracy of machine-based ATC readback monitoring. The core idea is to couple a plug-in open-set classifier with a carefully designed in-context learning mechanism on top of a frozen LLM. Extensive experiments on the semi-synthetic communication dataset show that SCOPE attains superior accuracy while delivering the low-latency response required for operational environments. Under a few-shot setting, SCOPE achieves 91.05% accuracy in open-set detection and corrects 96.63% of anomalous readbacks, thereby outperforming the strongest available baselines while providing explanations for its decisions. These findings demonstrate the potential of our framework as a practical pathway toward interpretable and controllable ATC readback monitoring.

Abstract

Explore similar work

SCOPE: A Lightweight-training LLM Framework for Air Traffic Control Readback Monitoring

Safety-Oriented Evaluation of Language Understanding Systems for Air Traffic Control

AeroCopilotBench: Safety-Gated Evaluation of LLM Agents on Aircraft Emergency Procedures in an Executable Cockpit