Establishing Qualitative Properties for Probabilistic Lossy Channel Systems: An Algorithmic Approach

Christel BaierChristel Baier, Bettina EngelenBettina Engelen

DOI Link

Christel Baier, Bettina Engelen
Establishing Qualitative Properties for Probabilistic Lossy Channel Systems: An Algorithmic Approach
Formal Methods for Real-Time and Probabilistic Systems, 5th International AMAST Workshop (ARTS), volume 1601 of Lecture Notes in Computer Science, 34--52, 1999. Springer

Details
Bibtex

KurzfassungAbstract
Lossy channel systems (LCSs) are models for communicating systems where the subprocesses are linked via unbounded FIFO channels which might lose messages. Link protocols, such as the Alternating Bit Protocol and HDLC can be modelled with these systems. The decidability of several verification problems of LCSs has been investigated by Abdulla & Jonsson [AJ93], AJ94], e.g. they have shown that the reach-ability problem for LCSs is decidable while LTL model checking is not. In this paper, we consider probabilistic LCSs (which are LCSs where the transitions are augmented with appropriate probabilities) as introduced by [IN97] and show that the question of whether or not a linear time property holds with probability 1 is decidable. More precisely, we show how LTL ∖X model checking for (certain types of) probabilistic LCSs can be reduced to a reachability problem in a (non-probabilistic) LCS where the latter can be solved with the methods of [AJ93].
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-48778-6_3.

@inproceedings{BE1999,
  author    = {Christel Baier and Bettina Engelen},
  title     = {Establishing Qualitative Properties for Probabilistic Lossy
               Channel Systems: An Algorithmic Approach},
  booktitle = {Formal Methods for Real-Time and Probabilistic Systems, 5th
               International {AMAST} Workshop (ARTS)},
  series    = {Lecture Notes in Computer Science},
  volume    = {1601},
  publisher = {Springer},
  year      = {1999},
  pages     = {34--52},
  doi       = {10.1007/3-540-48778-6_3}
}