Matthias Troffaes, Damjan Skulj

---

Model checking for imprecise Markov chains

Abstract

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.

Keywords

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

---

Download area

The paper is available in the following formats:

• pdf file

E-mail addresses

Matthias Troffaes		matthias.troffaes@gmail.com
Damjan Skulj		damjan.skulj@fdv.uni-lj.si/a>