zbMATH — the first resource for mathematics

Symbolic and parametric model checking of discrete-time Markov chains. (English) Zbl 1108.68497
Liu, Zhiming (ed.) et al., Theoretical aspects of computing – ICTAC 2004. First international colloquium, Guiyang, China, September 20–24, 2004. Revised selected papers. Berlin: Springer (ISBN 3-540-25304-1/pbk). Lecture Notes in Computer Science 3407, 280-294 (2005).
Summary: We present a language-theoretic approach to symbolic model checking of PCTL over discrete-time Markov chains. The probability with which a path formula is satisfied is represented by a regular expression. A recursive evaluation of the regular expression yields an exact rational value when transition probabilities are rational, and rational functions when some probabilities are left unspecified as parameters of the system. This allows for parametric model checking by evaluating the regular expression for different parameter values, for instance, to study the influence of a lossy channel in the overall reliability of a randomized protocol.
For the entire collection see [Zbl 1069.68010].

68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI