On Reachability for Unidirectional Channel Systems Extended with Regular Tests

TL;DR

This paper investigates the reachability problem in unidirectional channel systems with regular tests, showing decidability is maintained with emptiness tests but becomes undecidable with more general regular tests.

Contribution

It extends the understanding of reachability in channel systems by identifying the boundary between decidability and undecidability when adding regular channel tests.

Findings

Reachability remains decidable with emptiness and nonemptiness tests.

Regular tests beyond emptiness lead to undecidability.

Reduction to Post's Embedding Problem underpins the decidability proof.

Abstract

"Unidirectional channel systems" (Chambart & Schnoebelen, CONCUR 2008) are finite-state systems where one-way communication from a Sender to a Receiver goes via one reliable and one unreliable unbounded fifo channel. While reachability is decidable for these systems, equipping them with the possibility of testing regular properties on the contents of channels makes it undecidable. Decidability is preserved when only emptiness and nonemptiness tests are considered: the proof relies on an elaborate reduction to a generalized version of Post's Embedding Problem.