Sciweavers

ASIAN
2003
Springer

Model Checking Probabilistic Distributed Systems

14 years 4 months ago
Model Checking Probabilistic Distributed Systems
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 (LTL⊗ ). The main result of the paper is a model-checking procedure for PPA and LTL⊗ . With its help, it is possible to check qualitative properties of distributed systems automatically.
Benedikt Bollig, Martin Leucker
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where ASIAN
Authors Benedikt Bollig, Martin Leucker
Comments (0)