Reasoning about Probabilistic Lossy Channel Systems

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
Reasoning about Probabilistic Lossy Channel Systems
11th International Conference on Concurrency Theory (CONCUR), volume 1877 of Lecture Notes in Computer Science, 320--333, 2000. Springer

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 communicating over unbounded lossy FIFO channels. Abdulla and Jonsson have shown that safety properties are decidable while progress properties are not 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 show that the problem of checking whether a progress property holds with probability 1 is undecidable, if the assumption about “sufficiently high” probability of loss is omitted. More surprisingly, we show that checking whether safety properties hold with probability 1 is undecidable too. 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

The final publication is available at Springer via http://dx.doi.org/10.1007/3-540-44618-4_24.

@inproceedings{ABIJ2000,
  author    = {Parosh Aziz Abdulla and Christel Baier and S. Purushothaman Iyer
               and Bengt Jonsson},
  title     = {Reasoning about Probabilistic Lossy Channel Systems},
  booktitle = {11th International Conference on Concurrency Theory (CONCUR)},
  series    = {Lecture Notes in Computer Science},
  volume    = {1877},
  publisher = {Springer},
  year      = {2000},
  pages     = {320--333},
  doi       = {10.1007/3-540-44618-4_24}
}