PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Roberto Luvini, Giacomo Longo, Alessandro Armando, Enrico Russo

arXiv:2608.25926v1cs.AIcs.CLeess.AS

TL;DR

The paper addresses the difficulty of determining whether spoken ATC procedures satisfy applicable obligations across aircraft, states, and observations. It presents an executable runtime-verification framework that formalizes obligations and produces evidence-linked verdicts, with successful validation on real traffic, synthetic situations, and reconstructed accidents.

  • Problem

    Determining whether ongoing pilot-controller interactions satisfy all applicable obligations ultimately relies on human operators, despite growing traffic and constrained staffing in a safety-critical domain.

  • Method

    The framework converts radio exchanges into entity-linked events, integrates surveillance and onboard observations into time-stamped traces, and evaluates ICAO-derived temporal obligations with explicit deadlines and precedence.

  • Results

    The complete pipeline reaches an F1 of 0.85 on real traffic, the monitor logic returns the expected verdict in all 1,495 synthetic situations, and reconstructed accident cases match investigators’ reported deviations.

  • Takeaways & Limitations

    The monitor supports real-time assistance, post-operation review, and controller training by linking procedural deviations to failed obligations and supporting observations.

  • Takeaways & Limitations

    Aircraft dynamics and controllability remain beyond the monitor’s purview, so it identifies procedural deviations without modeling those aspects of aircraft behavior.

Abstract

from arXiv · show

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.

I. INTRODUCTION

The paper addresses the difficulty of continuously verifying spoken ATC procedures by introducing a runtime-verification framework that combines communications with operational evidence. It formalizes obligations and produces explainable verdicts, with evaluations on real traffic, synthetic situations, and documented accidents.

  • Motivation: ATC compliance cannot be assessed from transcripts alone because it requires linking utterances, participants, aircraft state, timing, and resulting obligations.The framework targets the human-dependent task of determining whether ongoing interactions satisfy all applicable obligations.
  • Requirements: The framework defines four requirements: observation grounding, multi-source integration, temporal reasoning, and evidence-backed verdicts.These requirements connect each deviation to the relevant aircraft, obligation, deadline, and supporting observations.
  • Motivation: 37 million scheduled departures in 2024 and more than 22.4 million minutes of European en-route delay illustrate the workload context for automated assistance.The paper places these pressures in a safety-critical domain where procedural deviations have contributed to documented accidents.
  • Approach: The proposed framework converts spoken exchanges into entity-linked events, merges them with surveillance and onboard state, and evaluates timed traces using temporal formulas.This gives procedural requirements precise semantics and makes compliance machine-checkable.
  • Contributions: The paper’s contributions include a temporal formalism with metric time bounds and precedence among obligations.It presents this as the first temporal-logic formalization of controller and pilot obligations, to the authors’ knowledge.
  • Evaluation: The framework reports verdicts linked to violated obligations and supporting observations, and its empirical evaluation covers real traffic, synthetic situations, and two documented accidents.The paper also identifies real-time assistance, post-operation review, and controller training as operational uses.

II. BACKGROUND

ATC monitoring compares intended actions expressed through radio exchanges with aircraft behavior observed through surveillance and onboard systems. The paper frames this comparison using temporal logic and validates it with complementary accident reconstructions.

  • Air traffic control procedures and monitoring sources: ATC procedures use standardized voice exchanges in which controllers issue instructions and pilots acknowledge or execute them.Call signs identify aircraft, while clearances and instructions specify authorized or required actions such as headings, speeds, and flight levels.
  • Air traffic control procedures and monitoring sources: Instruction compliance requires aircraft-state information, because radio exchanges specify intended actions whereas surveillance provides observed behavior.Compliance is the comparison between the two.
  • Air traffic control procedures and monitoring sources: Existing operational safety nets include conflict alerts for predicted separation-minima infringements and surface alerts for runway incursions.These systems provide established surveillance-derived monitoring functions in ATC operations.
  • Air traffic control procedures and monitoring sources: TCAS independently tracks nearby aircraft and issues climb or descent resolution advisories when collision risk becomes imminent.Its onboard advisories can constrain aircraft behavior separately from ATC instructions.
  • Temporal-logic specifications over finite traces: LTL and LTLf express and evaluate temporal properties over traces, while MTL adds explicit bounds on elapsed time and runtime verification checks observed behavior against specifications.These form the conceptual basis for timed procedural monitoring.
  • Validation scenarios: The two validation cases cover airborne and surface operations and combine radio, surveillance, and onboard observations in different proportions.Both were reconstructed from authoritative BFU and NTSB investigation reports and involved failures to meet procedural obligations.

B. Monitoring requirements exposed by the cases

The case analyses motivate a formal abstraction that links ATC concepts to aircraft and observed behavior, then evaluates procedural requirements over finite timed traces. The model represents operational facts as propositions and connects them through temporal formulas.

  • Monitoring requirements exposed by the cases: Official accident reports motivate evidence-backed verdicts by linking each procedural deviation to its obligation, aircraft, instant, and recorded observations.The paper uses the cases to show why observation grounding, multi-source integration, and temporal reasoning are also required.
  • Monitoring requirements exposed by the cases: In the Überlingen case, the deviation becomes visible only by associating the descent instruction and collision-avoidance advisories with the aircraft and its vertical motion.An active advisory commanded a climb while the controller’s standing instruction required descent, and the advisory took precedence.
  • Formal abstraction: The formal abstraction represents ATC concepts with atomic propositions, finite timed traces, and temporal formulas for monitored procedural requirements.The framework adopts finite-trace semantics because flights, exchanges, and recordings eventually end, while timestamps support deadlines.
  • Formal model: The formal model M = ⟨AP, Π, Φ, |=⟩ consists of atomic propositions, finite timed traces, a finite-trace temporal language, and a satisfaction relation.The satisfaction relation evaluates formulas at trace positions.
  • Atomic propositions: Atomic propositions collect ground facts over aeronautical entities, including aircraft, levels, headings, speeds, runways, agents, and utterances.Facts may represent spoken content, surveillance-derived state, or computed relations such as matching readbacks and active authorizations.
  • Atomic propositions: The proposition vocabulary separates speech, air-state, surface-state, and derived propositions, with some facts persisting until later observations end them.A descent example links controller instruction, pilot readback, and aircraft vertical motion through shared aircraft and level parameters.

B. Timed traces

A timed trace records timestamped observations and the propositions holding at each instant. Explicit, monotone timestamps preserve both event order and elapsed time, enabling procedural deadlines to be checked.

  • Timed traces: Each trace observation is a pair (t_i, L_i), where t_i is elapsed seconds and L_i is the set of propositions holding at that instant.A trace contains n ≥1 observations.
  • Timed traces: Explicit timestamps are necessary for deadlines because irregularly spaced observations cannot be interpreted from order alone.Timestamps are monotone, and equal timestamps are allowed when independent sources report simultaneously.
  • Timed traces: In the descent example, the instruction occurs at t = 0, the readback at t = 8, and surveillance reports descent at t = 20.The trace therefore captures both the ordering and unequal elapsed times among the three facts.

C. Temporal-logic patterns and ATC formula families

The framework organizes ATC obligations into recurring temporal-logic patterns, then specializes those patterns into extensible formula families with operational time bounds and precedence rules.

  • Five recurring logical patterns capture procedural dependencies such as response, compliance, precedence, and exception handling.
  • Temporal patterns: A bounded-response pattern requires every trigger α to be followed by β within δ seconds, using F≤δ for elapsed-time constraints.
  • Temporal patterns: Invariant formulas require β whenever α holds, while precedence formulas prohibit action α before authorization β.
  • Temporal patterns: Bounded-prohibition formulas forbid β within δ seconds after α, while weak-next guards avoid violations caused solely by reaching the trace end.
  • ATC formula families: ATC formula families instantiate these patterns with domain propositions and operational bounds; new procedures can be added as further instances.
  • ATC formula families: The families cover authorization, contingency, clearance precedence, repeated instructions, and advisory-direction constraints.

D. Evaluation semantics

The monitor evaluates temporal formulas over timed traces using finite-trace runtime-verification semantics, distinguishing definitive verdicts from obligations that remain unresolved online.

  • The satisfaction relation evaluates each formula at a trace position, yielding a verdict for the timed execution trace.
  • Formula semantics: The operators X, G, U, W, and F≤δ respectively encode successor, global, until, weak-until, and bounded-finally behavior over trace positions and timestamps.
  • Runtime monitoring: The monitor evaluates every formula from the first trace position, supporting offline analysis of completed recordings and online analysis of growing traces.
  • Runtime monitoring: Open traces use three-valued semantics: pending time-bounded obligations are reported as not-yet-violated until their deadlines pass.
  • Runtime monitoring: Globally scoped formulas become definitively true only when the recording ends, because later observations could still falsify them.
  • Explainable verdicts: Violations include the responsible position and propositions holding there, linking each verdict to supporting observations; verdicts remain relative to the captured trace.

V. VERIFICATION FRAMEWORK

The verification framework transforms heterogeneous operational inputs into a unified timed trace and evaluates formal procedural requirements over that trace.

  • The architecture comprises acquisition, atom extraction, trace construction, and verification stages.Offline processing uses completed recordings; online processing incrementally handles a growing trace.

A. Acquisition and atom extraction

Acquisition and atom extraction convert radio and surveillance data into formal observations representing spoken exchanges and aircraft state.

  • The first two stages transform radio and surveillance signals into ground atoms in the formal vocabulary.
  • Acquisition: Radio acquisition captures controller-pilot audio, while surveillance acquisition collects ADS-B aircraft-state messages; additional state streams can be incorporated.
  • Atom extraction: Atom extraction transcribes speech, parses utterances into speech atoms, and converts surveillance reports into state atoms; unmatched transcriptions are discarded.
  • Atom extraction: State decoding produces air-state atoms for level, position, and motion, and surface-state atoms for runway and taxiway occupancy.

B. Trace construction

The framework resolves speech and state observations into a time-ordered trace, incrementally derives additional atoms, and evaluates temporal formulas online or offline. Its monitor reports violations only when the evidence makes them decidable, while preserving explanations for each verdict.

  • Trace construction: Callsign resolution links speech atoms to aircraft by normalizing transcribed or abbreviated identifiers against surveillance identities.Unconfirmed callsigns are retained only when controller and pilot use them consistently; unresolved speech atoms are discarded.
  • Trace construction: Trace assembly orders resolved speech and state atoms by event time, then derives readback matches and propagates clearances as the trace grows.This prevents speech-recognition and decoding delays from changing timestamps used by temporal constraints.
  • Formula evaluation: The monitor selects formulas mentioning aircraft and values present in the trace, then evaluates them structurally against the timed trace.Metric operators compare timestamps with deadlines, and evaluation has worst-case quadratic complexity in trace length.
  • Online verdicts: Online monitoring inserts a virtual empty observation at the current instant so expired deadlines can be detected without waiting for another event.A violation requires falsity under both ordinary evaluation and evaluation treating unexpired metric obligations as satisfied; disagreement remains inconclusive.
  • Online verdicts: Open traces distinguish inconclusive and not-yet-violated obligations, while each detected violation identifies its responsible trace position and propositions.Closed recordings yield two-valued verdicts once all relevant deadlines have passed.
  • Implementation: The implementation combines faster-whisper and LLM-based structured parsing with Python modules for state decoding, callsign resolution, trace assembly, and formula evaluation.Online parsing uses qwen2.5-7b, whereas offline analysis uses qwen3.8-27b; inference runs on the GPU and other components on the CPU.

B. Datasets and vocabulary coverage

The evaluation uses two public traffic corpora paired with recoverable aircraft state and measures both vocabulary coverage and computational performance. Synthetic tests establish monitor correctness, while latency and accuracy analyses distinguish online from offline parser configurations.

  • Datasets: The evaluation combines ATCO2 and TartanAviation, the only publicly available corpora known to pair controller–pilot communications with recoverable aircraft state.ATCO2 is aligned with decoded OpenSky ADS-B vectors, while TartanAviation provides synchronized radio communications and ADS-B trajectories.
  • Vocabulary coverage: 37.6% of routine schemas are exercised across both corpora.Coverage excludes exceptional events such as emergencies, runway incursions, and collision scenarios, which are absent from the corpora.
  • Synthetic evaluation: 1,495 synthetic situations comprise 664 compliant and 831 violating cases, exercising 50 forms across five of eight formula families.These situations are constructed from real corpus events because safety-critical configurations are rare and cannot be deliberately induced in live traffic.
  • Evaluation results: The monitor returns the expected verdict in every synthetic situation.The pipeline is additionally scored on a three-hour ground-truth real-traffic set using precision, recall, and F1 across three parser models.
  • Processing cost: Speech recognition runs faster than real time, while parsing is the largest computational-cost component and formula evaluation contributes a smaller but more variable share.Table III reports minimum, Q1, median, Q3, and maximum costs for each stage measured separately.
  • Accuracy–latency trade-off: The no-thinking qwen3.8-27b achieves the highest F1 at moderate latency, whereas qwen2.5-7b has the lowest latency with reduced F1.The 7B parser is selected for online monitoring, while no-thinking qwen3.8-27b serves as the offline reference parser.

E. Documented accidents

The monitor was replayed on two historically documented accidents reconstructed from official reports, identifying investigators’ reported procedural deviations and providing detection timing relevant to alerts.

  • Case-study validation: In both reconstructed accidents, monitor firings agreed in content and timing with the events documented by official investigators.The cases tested rare safety-critical situations outside the evaluation corpora, without accuracy metrics.
  • Detection timing: The monitor places each violation when its formula is decided after the triggering deadline, so reported detection instants can trail earlier documented events.Investigation-report wall-clock times are mapped from session-relative monitor time.
  • Überlingen: In Überlingen, the monitor detected the collision-avoidance climb during descent, confirmed the resolution advisory, and flagged that the advisory was not reported to the controller.These detections matched the BFU-documented sequence in the reconstructed radio, avionics, and surveillance state.
  • Comair 5191: In Comair 5191, the monitor detected the wrong call sign, a takeoff clearance without a runway, runway entry, and the associated runway-incursion checks.The detections used radio and position-track evidence, though some firings followed the documented hold-short crossing because surface entry was resolved later.
  • Operational uses: The framework’s operational uses include real-time assistance, post-operation review, and controller training with evidence-linked procedural feedback.Early detection may create an intervention window, while recorded sessions can use a more accurate offline parser.

VIII. RELATED WORK

Related approaches address different subsets of spoken ATC monitoring requirements, whereas this work combines entity grounding, multi-source integration, temporal reasoning, and evidence-backed verdicts.

  • Coverage landscape: Existing approaches variously cover restricted surveillance timing, voice-based readback checks, combined voice and ADS-B checks, or formula-level explanations.Table IV compares representative methods against the four requirements introduced in the paper.
  • Surveillance approaches: Surveillance-only monitoring partially addresses temporal reasoning but excludes radio input and does not identify breached obligations or supporting observations.Reynolds et al. compare observed tracks with trajectories expected from active clearances.
  • Voice approaches: Voice-based readback monitoring grounds utterances in addressed aircraft and values, but does not use surveillance in the compliance decision or verify the maneuver flown.Its compliance check stops at the pilot readback.
  • Combined approaches: Combined voice-and-surveillance monitoring meets grounding and multi-source integration, but fixed validity windows and non-superseding instructions provide only partial temporal reasoning.Lin et al. evaluate repetition, conflicts, and conformance with instructed maneuvers using ADS-B tracks.
  • Runtime verification: Runtime-verification monitors can express deadlines and ordering, yet prior work may lack links from verdicts to operational observations or may assume logical traces as input.Lima et al. provide formula-level proofs, while trajectory-based methods use a single observation source.
  • This work: The paper positions its framework as jointly addressing the four requirements that related approaches cover separately or only partially.Its conclusion describes grounding communications, integrating surveillance and onboard observations, using timed obligations, and linking violations to evidence.
Loading 2608.25926v1…