Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

20

ASIAN
2003
Springer

favoriteEmaildiscussreport

170views Algorithms» more ASIAN 2003»

Model Checking Probabilistic Distributed Systems

13 years 9 months ago

Model Checking Probabilistic Distributed Systems

Download www4.in.tum.de

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

Real-time Traffic

ASIAN 2003 | Distributed Systems | Leader Election Protocols | Probabilistic Product Automata |

claim paper

Related Content

» Model checking for probability and time from theory to practice

» ProbVerus Probabilistic Symbolic Model Checking

» Using probabilistic model checking in systems biology

» Counterexamples in Probabilistic LTL Model Checking for Markov Chains

» Symbolic Model Checking for Probabilistic Timed Automata

» Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Represen...

» Partial Order Reduction for Probabilistic Systems A Revision for Distributed Schedulers

» On Model Checking Techniques for Randomized Distributed Systems

» Probabilistic Model Checking of Complex Biological Pathways

Post Info
More Details (n/a)

Added	06 Jul 2010
Updated	06 Jul 2010
Type	Conference
Year	2003
Where	ASIAN
Authors	Benedikt Bollig, Martin Leucker

Comments (0)