Automata and Logics for Distributed Systems

Automata are a popular model of computer systems, making them accessible to formal methods and, in particular, synthesis and model checking. While classical finite-state automata are suitable to model sequential boolean programs, models of distributed and concurrent systems involve several interacting processes and extend finite-state machines in many respects. Roughly, we may classify system models according to their communication paradigm (shared variables, message passing, broadcasting), the type of a process (finite-state, recursive, timed), or the number of processes (static, dynamic, bounded, parameterized). In this tutorial, we survey automata models for several combinations of the above-mentioned characteristics. We also present suitable specification formalisms such as monadic second-order logic, temporal logic, and rational expressions. In particular, we will compare the expressive power of automata and logics, give translations of specifications into automata, and show how to solve the model-checking problem: Does a given automaton satisfy its specification?

Authors

• Benedikt Bollig (LSV
• ENS Cachan)

Keywords

No keywords are indexed for this paper.