| Description |
Markov chains are omnipresent. They are used as semantical backbone of Markovian queueing networks, stochastic Petri nets, stochastic process algebras, and calculi for systems biology. Abundant applications in performance, reliability and dependability analysis use Markov chains. The specification of measures-of-interest is however quite limited, and dedicated algorithms are typically developed for every new measure.
In this talk, we will survey model checking techniques for Markov chains. On the one hand, temporal logics allow to express most measures of interest as well as measures that go beyond the classical one. On the other hand, a single model-checking algorithm suffices to deal with all measures that can be expressed.
We will describe the basic model-checking algorithms, covering both discrete-time and continuous-time Markov chains, and report on recent progress on using timed automata as requirements (rather than temporal logic).
|