Compiegne ISIPTA'11 home
Latest info: Pictures now online.

Matthias Troffaes, Damjan Skulj

Model checking for imprecise Markov chains


We extend probabilistic computational tree logic for expressing properties of Markov chains to imprecise Markov chains, and provide an efficient algorithm for model checking of imprecise Markov chains. Thereby, we provide a formal framework to answer a very wide range of questions about imprecise Markov chains, in a systematic and computationally efficient way.


imprecise Markov chain, model checking, parse tree, logic, computation

Download area

The paper is available in the following formats:

E-mail addresses

Matthias Troffaes
Damjan Skulj>

Send any remarks to