Reachability problems for communicating finite state machines

TL;DR

This paper investigates the decidability of reachability problems in communication protocols modeled by finite state machines with FIFO channels, focusing on the recognizable and rational channel properties.

Contribution

It clarifies the decidability status for protocols with rational channels, extending understanding beyond the known results for recognizable channels.

Findings

Reachability is decidable for protocols with recognizable channel property.

Decidability remains open for protocols with rational channel property.

Provides a theoretical framework for analyzing communication protocol verification.

Abstract

The paper deals with the verification of reachability properties in a commonly used state transition model of communication protocols, which consists of finite state machines connected by potentially unbounded FIFO channels. Although simple reachability problems are undecidable for general protocols with unbounded channels, they are decidable for the protocols with the recognizable channel property. The decidability question is open for the protocols with the rational channel property.