Inproceedings1920928405: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Johannes Lehmann (Diskussion | Beiträge) (Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Christel |ErsterAutorNachname=Baier |FurtherAuthors=Nathalie Bertrand; Philippe Schnoebelen}} {{Inproceedings |Booktitle=Proc. of the 26th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE) |Pages=212--227 |Publisher=Springer |Series=Lecture Notes in Computer Science |Title=Symbolic Verification of Communicating Systems with Probabilistic Message L…“) |
Johannes Lehmann (Diskussion | Beiträge) K (Textersetzung - „Verifikation und formale quantitative Analyse“ durch „Algebraische und logische Grundlagen der Informatik“) |
||
| Zeile 15: | Zeile 15: | ||
|DOI Name=10.1007/11888116_17 | |DOI Name=10.1007/11888116_17 | ||
|Abstract=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. | |Abstract=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= | |Forschungsgruppe=Algebraische und logische Grundlagen der Informatik | ||
}} | }} | ||
Aktuelle Version vom 5. März 2025, 15:45 Uhr
Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness
Christel BaierChristel Baier, Nathalie BertrandNathalie Bertrand, Philippe SchnoebelenPhilippe Schnoebelen
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
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
- 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
@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}
}
