Model checking Probabilistic Distributed Systems
| Title | Model checking Probabilistic Distributed Systems |
| Publication Type | Conference Paper |
| Year of Publication | 2003 |
| Authors | Benedikt Bollig, Leucker, M |
| Conference Name | Proceedings of the 8th Asian Computing Science Conference ({ASIAN'03}) |
| Series | Lecture Notes in Computer Science |
| Volume | 2896 |
| Publisher | Springer |
| Conference Location | Mumbai, India |
| Abstract | Protocols for distributed systems make often use of random transitions to achieve a common goal. A popular example are randomized leader election protocols. We introduce probabilistic product automata (PPA) as a natural model for this kind of systems. To reason about these systems, we propose to use a product version of linear temporal logic (PLTL). The main result of the paper is a model-checking procedure for PPA and PLTL. With its help, it is possible to check qualitative properties of distributed systems automatically. |
| URL | http://www.springerlink.com/media/g3t6cbhd4jcrng83ng86/Contributions/C/3/P/6/C3P6MDCKUFXABH8U_html/fulltext.html |
Bibtex:
@inproceedings {BolligLeucker03,
title = {Model checking Probabilistic Distributed Systems},
booktitle = {Proceedings of the 8th Asian Computing Science Conference ({ASIAN{\textquoteright}03})},
series = {Lecture Notes in Computer Science},
volume = {2896},
year = {2003},
pages = {291{\textendash}304},
publisher = {Springer},
organization = {Springer},
address = {Mumbai, India},
abstract = {Protocols for distributed systems make often use of random transitions to achieve a common goal. A popular example are randomized leader election protocols. We introduce probabilistic product automata (PPA) as a natural model for this kind of systems. To reason about these systems, we propose to use a product version of linear temporal logic (PLTL). The main result of the paper is a model-checking procedure for PPA and PLTL. With its help, it is possible to check qualitative properties of distributed systems automatically.},
url = {http://www.springerlink.com/media/g3t6cbhd4jcrng83ng86/Contributions/C/3/P/6/C3P6MDCKUFXABH8U_html/fulltext.html},
author = {Benedikt Bollig and Martin Leucker}
}PDF:
Postscript:
