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.

• Type: Conference
• Year: 2003
• Where: ASIAN
• Authors: Benedikt Bollig, Martin Leucker
• Keywords: ASIAN 2003, Distributed Systems, Leader Election Protocols, Probabilistic Product Automata