Simulating perfect channels with probabilistic lossy channels

Parosh Aziz AbdullaParosh Aziz Abdulla, Christel BaierChristel Baier, S. Purushothaman IyerS. Purushothaman Iyer, Bengt JonssonBengt Jonsson

DOI Link

Parosh Aziz Abdulla, Christel Baier, S. Purushothaman Iyer, Bengt Jonsson
Simulating perfect channels with probabilistic lossy channels
Information and Computation, 197(1--2):22--40, 2005

Details
Bibtex

KurzfassungAbstract
We consider the problem of deciding whether an infinite-state system (expressed as a Markov chain) satisfies a correctness property with probability 1. This problem is, of course, undecidable for general infinite-state systems. We focus our attention on the model of probabilistic lossy channel systems consisting of finite-state processes that communicate over unbounded lossy FIFO channels. Abdulla and Jonsson have shown that safety properties are decidable while progress properties are undecidable for non-probabilistic lossy channel systems. Under assumptions of “sufficiently high” probability of loss, Baier and Engelen have shown how to check whether a property holds of probabilistic lossy channel system with probability 1. In this paper, we consider a model of probabilistic lossy channel systems, where messages can be lost only during send transitions. In contrast to the model of Baier and Engelen, once a message is successfully sent to channel, it can only be removed through a transition which receives the message. We show that checking whether safety properties hold with probability 1 is undecidable for this model. Our proof depends upon simulating a perfect channel, with a high degree of confidence, using lossy channels.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@article{ABIJ2005,
  author  = {Parosh Aziz Abdulla and Christel Baier and S. Purushothaman Iyer
             and Bengt Jonsson},
  title   = {Simulating perfect channels with probabilistic lossy channels},
  journal = {Information and Computation},
  volume  = {197},
  number  = {1--2},
  year    = {2005},
  pages   = {22--40},
  doi     = {10.1016/J.IC.2004.12.001}
}