An automata-theoretic approach to the verification of distributed algorithms

摘要

We introduce an automata-theoretic method for the verification of distributed algorithms running on ring networks. In a distributed algorithm, an arbitrary number of processes cooperate to achieve a common goal (e.g., elect a leader). Processes have unique identifiers (pids) from an infinite, totally ordered domain. An algorithm proceeds in synchronous rounds, which allow processes to exchange pids, store them in registers, and compare their register contents. To specify correctness properties, we introduce a logic that can reason about processes and pids. We show that model checking distributed algorithms can be reduced to satisfiability in propositional dynamic logic with loop and converse. Using this reduction, we provide an automata-theoretic approach to proving distributed algorithms correct up to a given number of rounds. Overall, we show that round-bounded verification of distributed algorithms over rings is PSPACE-complete, provided the number of rounds is given in unary.