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 (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. © Springer-Verlag Berlin Heidelberg 2003.
Cite
CITATION STYLE
Bollig, B., & Leucker, M. (2003). Model checking probabilistic distributed systems. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2896, 291–304. https://doi.org/10.1007/978-3-540-40965-6_19
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
