Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Synchronizability of Communicating Finite State Machines is not Decidable

Alain Finkel, Etienne Lozes

TL;DR

The paper investigates the decidability of synchronizability for systems of communicating finite state machines (CFSMs). It proves that synchronizability is undecidable for systems with at least three peers under the peer-to-peer FIFO model, and shows that the small-model property fails for both mailbox and peer-to-peer semantics, invalidating prior decidability claims. Conversely, it establishes decidability for oriented-ring topologies, leveraging confluence and trace normalization to prove that 1-synchronizability implies full synchronizability and that the reachability set is channel-recognizable. These results collectively illuminate the boundaries between decidability and undecidability in CFSM synchronization and identify precise conditions under which buffer-scaled behavior can be faithfully analyzed. The findings have implications for choreography realizability and the verification of distributed protocols across different communication models and topologies.

Abstract

A system of communicating finite state machines is synchronizable if its send trace semantics, i.e.the set of sequences of sendings it can perform, is the same when its communications are FIFO asynchronous and when they are just rendez-vous synchronizations. This property was claimed to be decidable in several conference and journal papers for either mailboxes or peer-to-peer communications, thanks to a form of small model property. In this paper, we show that this small model property does not hold neither for mailbox communications, nor for peer-to-peer communications, therefore the decidability of synchronizability becomes an open question. We close this question for peer-to-peer communications, and we show that synchronizability is actually undecidable. We show that synchronizability is decidable if the topology of communications is an oriented ring. We also show that, in this case, synchronizability implies the absence of unspecified receptions and orphan messages, and the channel-recognizability of the reachability set.

Synchronizability of Communicating Finite State Machines is not Decidable

TL;DR

The paper investigates the decidability of synchronizability for systems of communicating finite state machines (CFSMs). It proves that synchronizability is undecidable for systems with at least three peers under the peer-to-peer FIFO model, and shows that the small-model property fails for both mailbox and peer-to-peer semantics, invalidating prior decidability claims. Conversely, it establishes decidability for oriented-ring topologies, leveraging confluence and trace normalization to prove that 1-synchronizability implies full synchronizability and that the reachability set is channel-recognizable. These results collectively illuminate the boundaries between decidability and undecidability in CFSM synchronization and identify precise conditions under which buffer-scaled behavior can be faithfully analyzed. The findings have implications for choreography realizability and the verification of distributed protocols across different communication models and topologies.

Abstract

A system of communicating finite state machines is synchronizable if its send trace semantics, i.e.the set of sequences of sendings it can perform, is the same when its communications are FIFO asynchronous and when they are just rendez-vous synchronizations. This property was claimed to be decidable in several conference and journal papers for either mailboxes or peer-to-peer communications, thanks to a form of small model property. In this paper, we show that this small model property does not hold neither for mailbox communications, nor for peer-to-peer communications, therefore the decidability of synchronizability becomes an open question. We close this question for peer-to-peer communications, and we show that synchronizability is actually undecidable. We show that synchronizability is decidable if the topology of communications is an oriented ring. We also show that, in this case, synchronizability implies the absence of unspecified receptions and orphan messages, and the channel-recognizability of the reachability set.

Paper Structure

This paper contains 26 sections, 22 theorems, 32 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Messages and topologies
  4. Traces
  5. Peers, systems, configurations
  6. Synchronizability.
  7. Undecidability of Synchronizability
  8. An Undecidable Problem on FIFO automata
  9. A System that Simulates a FIFO Automaton
  10. A Synchronizable System
  11. Reducing the Message Reception Problem to Synchronizability
  12. The case of oriented rings
  13. Confluence properties
  14. Trace normalization
  15. Reachability set
  16. ...and 11 more sections

Key Result

Theorem 2.4

There is a system $\mathcal{S}$ that is $1$-synchronizable, but not synchronizable.

Figures (7)

  • Figure 1: System of Example \ref{['ex:counter-example-peer-to-peer']} and Theorem \ref{['thm:bugBultan']}.
  • Figure 2: The FIFO automaton $\mathcal{A}$ of Example \ref{['ex:fifo-automaton-encoding']} and its associated systems $\mathcal{S}_{\mathcal{A}}=\langle\mathcal{P}_1,\mathcal{P}_2,\mathcal{P}_3\rangle$ and $\mathcal{S}_{\mathcal{A},\underline{m}}'=\langle\mathcal{P}_1,\mathcal{P}_2',\mathcal{P}_3\rangle$. The sink state $q_{\bot}$ and the transitions $q\xrightarrow{?\underline{m}^{3\to 2}}q_{\bot}$ are omitted in the representation of $\mathcal{P}_2'$.
  • Figure 3: Diagrammatic representation of Lemma \ref{['lem:send-send-diagram']}
  • Figure 4: Diagram of Lemma \ref{['lem:lemaux-2']}
  • Figure 5: Diagram of Lemma \ref{['lem:lemaux-3']}
  • ...and 2 more figures

Theorems & Definitions (54)

  • Example 2.1
  • Example 2.2
  • Definition 2.3: Synchronizability BasuB11BasuBO12
  • Theorem 2.4
  • proof
  • Remark 2.5
  • Definition 3.1: Message reception problem
  • Remark 3.2
  • Lemma 3.3
  • proof
  • ...and 44 more