Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness

Christel BaierChristel Baier, Nathalie BertrandNathalie Bertrand, Philippe SchnoebelenPhilippe Schnoebelen

DOI Link

Christel Baier, Nathalie Bertrand, Philippe Schnoebelen
Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness
Proc. of the 26th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), volume 4229 of Lecture Notes in Computer Science, 212--227, 2006. Springer

Details
Bibtex

KurzfassungAbstract
NPLCS’s are a new model for nondeterministic channel systems where unreliable communication is modeled by probabilistic message losses. We show that, for ω-regular linear-time properties and finite-memory schedulers, qualitative model-checking is decidable. The techniques extend smoothly to questions where fairness restrictions are imposed on the schedulers. The symbolic procedure underlying our decidability proofs has been implemented and used to study a simple protocol handling two-way transfers in an unreliable setting.
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/11888116_17.

@inproceedings{BBS2006,
  author    = {Christel Baier and Nathalie Bertrand and Philippe Schnoebelen},
  title     = {Symbolic Verification of Communicating Systems with Probabilistic
               Message Losses: Liveness and Fairness},
  booktitle = {Proc. of the 26th {IFIP} {WG} 6.1 International Conference on
               Formal Techniques for Networked and Distributed Systems (FORTE)},
  series    = {Lecture Notes in Computer Science},
  volume    = {4229},
  publisher = {Springer},
  year      = {2006},
  pages     = {212--227},
  doi       = {10.1007/11888116_17}
}