---
title: "Formal, Executable and Explainable Runtime Monitoring of Spoken Air Traffic Control Operational Procedures"
source: "arXiv AI/CL/LG（论文）"
source_tier: "t2"
url: "https://arxiv.org/abs/2608.25926v1"
permalink: "https://feed.astralor.com/items/itm_553568786d17ccfa87c1e30f"
published: "2026-08-26T15:37:00.000Z"
score: 72
channel: "ai"
tags: ["Air Traffic Control","arXiv","ICAO","Runtime Verification","Temporal Logic"]
---

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

## AI commentary

> This paper combines formal methods with speech recognition, offering a practical new angle for aviation safety monitoring. It is worth reading for those working on NLP deployment and explainable AI in high-stakes domains.

## At a glance

Air traffic control procedures are executed through spoken exchanges between controllers and pilots, and failures can create severe hazards. This paper presents a runtime verification framework that parses radio communications into entity-linked events, merges them with surveillance and onboard observations into a timestamped trace, and evaluates ICAO-derived obligations formalized as temporal formulas with explicit time bounds. The pipeline reaches an F1 of 0.85 against blind human-annotated violations on real traffic, returns expected verdicts in all 1,495 synthetic situations, and identifies the same procedural deviations as official reports in two historical accidents.

## Key points

- An end-to-end runtime monitoring framework that combines speech parsing, surveillance data, and onboard observations to automatically detect procedural violations in ATC communications.
- ICAO obligations are formalized as temporal formulas with explicit time bounds, enabling explainable violation reports.
- Achieves F1 of 0.85 on real traffic, perfect verdicts on 1,495 synthetic situations, and matches official investigations in two historical accidents.

## Full text

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.

---

Verify against the original before citing; curated by Astral Feed: https://feed.astralor.com/items/itm_553568786d17ccfa87c1e30f