Probabilistic model checking
Dr Marta Kwiatkowska, School of Computer Science, University of Birmingham

Abstract: Probabilistic analysis can establish that certain properties hold (in some meaningful probabilistic sense) where conventional model checkers fail, either because the property simply is not true in the state (but holds in that state with some acceptable probability), or because exhaustive search of only a portion of the system is feasible. Models used for such analyses are variants of probabilistic automata (such as labelled Markov chains), in which the usual (boolean) transition relation is replaced with its probabilistic version given in the form of a transition probability matrix. We consider a probabilistic temporal logic PCTL, based on CTL, which allows one to express properties such as ``the probability of the message being delivered is at least 0.98''. Model checking procedure for this logic can be reduced to a linear programming problem. We show how Multi-Terminal Binary Decision Diagrams, a generalization of OBDDs due to Clarke et al, can be used as a basis for symbolic model checking for probabilistic systems.

This seminar was held at the Department of Computer Science, Royal Holloway, University of London on 17 March 1999.

back