Formal Guarantees of Timely Progress for Distributed Knowledge Propagation

TL;DR

This paper introduces a probabilistic approach to formally guarantee timely progress in distributed knowledge propagation protocols for urban air mobility, addressing the challenges of unbounded delays in asynchronous airborne networks.

Contribution

It develops a probabilistic model for guaranteeing progress in distributed protocols and creates a formal theory library in Athena for airborne network reasoning.

Findings

Probabilistic upper bounds on progress time are derived.

The approach models delays using Multicopy Two-Hop Relay and M/M/1 queue theories.

A formal library in Athena supports reasoning about timely progress in airborne protocols.

Abstract

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.