Formal Guarantees of Timely Progress for Distributed Knowledge Propagation
This work addresses the critical need for reliable coordination in time-sensitive urban air mobility operations, offering incremental improvements through formal verification of existing protocols.
The paper tackles the problem of ensuring timely progress in distributed protocols for autonomous air traffic management by providing formal probabilistic guarantees on delay bounds, using a Two-Phase Acknowledge protocol modeled with Multicopy Two-Hop Relay and M/M/1 queue theories, and developing a library in the Athena proof assistant for reasoning about such protocols.
Autonomous air traffic management (ATM) operations for urban air mobility (UAM) will necessitate the use of distributed protocols for decentralized coordination between aircraft. As UAM operations are time-critical, it will be imperative to have formal guarantees of progress for the distributed protocols used in ATM. Under asynchronous settings, message transmission and processing delays are unbounded, making it impossible to provide deterministic bounds on the time required to make progress. We present an approach for formally guaranteeing timely progress in a Two-Phase Acknowledge distributed knowledge propagation protocol by probabilistically modeling the delays using theories of the Multicopy Two-Hop Relay protocol and the M/M/1 queue system. The guarantee states a probabilistic upper bound to the time for progress as a function of the probabilities of the total transmission and processing delays being less than two given values. We also showcase the development of a library of formal theories, that is tailored towards reasoning about timely progress in distributed protocols deployed in airborne networks, in the Athena proof assistant.