Probabilistic model checking: Formalisms and algorithms for discrete and real-time systems

This paper considers the problem of verification of probabilistic systems, for both the discrete- and real-time cases. Probabilistic systems are modeled as Markov chains, concurrent Markov chains (i.e. MCs with non-determinism) or, in the real-time case, generalized semi-Markov processes (Markovian processes with time delays on events). Discrete-time specifications are described in the logics PTL (propositional temporal logic), ETL (extended temporal logic) or PCTL* (probabilistic full computation tree logic), or as Buchi automata. Real-time specifications are described either in TCTL (timed computation tree logic) or as deterministic timed Muller automata. The problems considered are either the probabilistic satisfaction of a specification by a system (i.e., satisfaction with probability one) or the computation of the satisfaction probability. We give complexity results for the above problems and present some of the corresponding algorithms. Finally, we illustrate the approach with some examples.