We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.DC

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Distributed, Parallel, and Cluster Computing

Title: Formal Guarantees of Timely Progress for Distributed Knowledge Propagation

Authors: Saswata Paul (Rensselaer Polytechnic Institute), Stacy Patterson (Rensselaer Polytechnic Institute), Carlos Varela (Rensselaer Polytechnic Institute)
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.
Comments: In Proceedings FMAS 2021, arXiv:2110.11527
Subjects: Distributed, Parallel, and Cluster Computing (cs.DC); Logic in Computer Science (cs.LO); Multiagent Systems (cs.MA); Software Engineering (cs.SE)
Journal reference: EPTCS 348, 2021, pp. 73-91
DOI: 10.4204/EPTCS.348.5
Cite as: arXiv:2110.12587 [cs.DC]
  (or arXiv:2110.12587v1 [cs.DC] for this version)

Submission history

From: EPTCS [view email]
[v1] Mon, 25 Oct 2021 01:55:41 GMT (62kb,D)

Link back to: arXiv, form interface, contact.