Communicating Finite-State Machines and Two-Variable Logic

TL;DR

This paper establishes an equivalence between communicating finite-state machines and a specific logical framework, enhancing understanding of their expressive power in formal verification.

Contribution

It proves that communicating finite-state machines are expressively equivalent to existential MSO logic with two variables and order, linking automata theory and logic.

Findings

Equivalence between communicating finite-state machines and existential MSO logic with two variables.

Provides a logical characterization of the expressive power of communicating finite-state machines.

Enhances formal methods for analyzing concurrent systems.

Abstract

Communicating finite-state machines are a fundamental, well-studied model of finite-state processes that communicate via unbounded first-in first-out channels. We show that they are expressively equivalent to existential MSO logic with two first-order variables and the order relation.