On decidability of simulation and bisimulation for Lossy Channel Systems

Parosh Aziz Abdullah
Mats Kindahl

In 6th NWPT, pages 67-77

Abstract:

By using an infinite-state system consisting of finite-state processes communicating via unbounded FIFO channels it is possible to model link protocols like the Alternating Bit protocol , or the HDLC protocol. It is well known that most interesting verification problems are undecidable for this class of systems. We have previously shown that by altering the behaviour of the channels so that they become lossy, several verification problems become decidable. In this paper we develop algorithms for deciding strong bisimulation equivalence and simulation preorder. Furthermore, we show that weak bisimulation equivalence is undecidable.

Comments
Uppsala, Sweden.

Available as PostScript.

BRICS WWW home page