Reasoning about Probabilistic Lossy Channel Systems
From International Center for Computational Logic
Reasoning about Probabilistic Lossy Channel Systems
Parosh Aziz AbdullaParosh Aziz Abdulla, Christel BaierChristel Baier, S. Purushothaman IyerS. Purushothaman Iyer, Bengt JonssonBengt Jonsson
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
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
- 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
@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}
}