Distributed Graph Automata and Verification of Distributed Algorithms
Formal Languages and Automata Theory
2018-07-03 v2 Distributed, Parallel, and Cluster Computing
Logic in Computer Science
Abstract
Combining ideas from distributed algorithms and alternating automata, we introduce a new class of finite graph automata that recognize precisely the languages of finite graphs definable in monadic second-order logic. By restricting transitions to be nondeterministic or deterministic, we also obtain two strictly weaker variants of our automata for which the emptiness problem is decidable. As an application, we suggest how suitable graph automata might be useful in formal verification of distributed algorithms, using Floyd-Hoare logic.
Cite
@article{arxiv.1408.3030,
title = {Distributed Graph Automata and Verification of Distributed Algorithms},
author = {Fabian Reiter},
journal= {arXiv preprint arXiv:1408.3030},
year = {2018}
}
Comments
26 pages, 6 figures, includes a condensed version of the author's Master's thesis arXiv:1404.6503. (This version of the article (v2) is identical to the previous one (v1), except for minor changes in phrasing.)