Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms
Nathalie Bertrand, Bastien Thomas, Josef Widder · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2021
Distributed algorithms typically run over arbitrary many processes and may involve unboundedly many rounds, making the automated verification of their correctness challenging. Building on domain theory, we introduce a framework that abstracts infinite-state distributed systems that represent distributed algorithms into finite-state guard automata. The soundness of the approach corresponds to the Scott-continuity of the abstraction, which relies on the assumption that the distributed algorithms are layered. Guard automata thus enable the verification of safety and liveness properties of distributed algorithms.