2026-07-21T14:13:07Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:14392 2024-03-06T10:54:17Z ddc:004 open_access

Guard Automata for the Verification of Safety and Liveness of Distributed Algorithms Bertrand, Nathalie Thomas, Bastien Widder, Josef Verification Distributed algorithms Domain theory 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Nathalie Bertrand and Bastien Thomas and Josef Widder 2021 Is Part Of LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2021.15 urn:nbn:de:0030-drops-143926 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.15 eng https://creativecommons.org/licenses/by/4.0/legalcode