The Community for Technology Leaders
Logic in Computer Science, Symposium on (2003)
Ottawa, Canada
June 22, 2003 to June 25, 2003
ISSN: 1043-6871
ISBN: 0-7695-1884-2
pp: 351
Marta Kwiatkowska , University of Birmingham
ABSTRACT
Probability features increasingly often in software and hardware systems: it is used in distributed coordination and routing problems, to model fault-tolerance and performance, and to provide adaptive resource management strategies. Probabilistic model checking is an automatic procedure for establishing if a desired property holds in a probabilistic model, aimed at verifying probabilistic specifications such as "leader election is eventually resolved with probability 1", "the chance of shutdown occurring is at most 0.01%", and "the probability that a message will be delivered within 30ms is at least 0.75". A probabilistic model checker calculates the probability of a given temporal logic property being satisfied, as opposed to validity. In contrast to conventional model checkers, which rely on reachability analysis of the underlying transition system graph, probabilistic model checking additionally involves numerical solutions of linear equations and linear programming problems. This paper reports our experience with implementing PRISM (www.cs.bham.ac.uk/~dxp/ prism/), a Probabilistic Symbolic Model Checker, demonstrates its usefulness in analysing real-world probabilistic protocols, and outlines future challenges for this research direction.
INDEX TERMS
null
CITATION
Marta Kwiatkowska, "Model checking for probability and time: from theory to practice", Logic in Computer Science, Symposium on, vol. 00, no. , pp. 351, 2003, doi:10.1109/LICS.2003.1210075
87 ms
(Ver 3.3 (11022016))