Communicating Finite-State Machines and Two-Variable Logic

Abstract:

In the early 1960s, Büchi, Elgot, and Trakhtenbrot showed that finite automata over words have the same expressive power as monadic second-order (MSO) logic. Since then, this fundamental theorem has been generalized to various other computational devices such as tree automata, asynchronous automata, nested-word automata, and branching automata. Actually, all these devices are complementable, which allows for an inductive translation of formulas into automata. In this talk, we consider communicating finite-state machines (CFMs), introduced by Brand and Zafiropulo in 1983. CFMs are a basic model of finite-state processes that communicate via unbounded FIFO channels. Unfortunately, they are not complementable. In fact, they are strictly less expressive than MSO logic (interpreted over certain partial orders). Nevertheless, CFMs enjoy logical characterizations in terms of fragments of MSO logic. We will show that CFMs are expressively equivalent to existential MSO logic with two first-order variables. As the main feature, the logic supports the happens-before relation, which reflects causality in an execution of a distributed system.

 This is joint work with Marie Fortin and Paul Gastin.