%0 Conference Proceedings
%F BBS-forte06
%A Baier, C.
%A Bertrand, N.
%A Schnoebelen, Ph.
%T Symbolic verification of communicating systems with probabilistic message losses: liveness and fairness
%B {P}roceedings of 26th {IFIP} {WG6.1} {I}nternational {C}onference on {F}ormal {T}echniques for {N}etworked and {D}istributed {S}ystems ({FORTE}'06)
%E Najm, Elie
%E Pradat-Peyre, Jean-Francois
%E Vigui\' Donzeau-Gouge, Véronique
%V 4229
%P 212-227
%S Lecture Notes in Computer Science
%I Springer
%C Paris, France
%X NPLCS’s are a new model for nondeterministic channel systems where unreliable communication is modeled by probabilistic message losses. We show that, for omega-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
%U http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-forte06.pdf
%U http://dx.doi.org/10.1007/11888116_17
%8 September
%D 2006