Model checking linear-time properties of probabilistic systems

Christel BaierChristel Baier, Marcus GrößerMarcus Größer, Frank CiesinskiFrank Ciesinski

DOI Link

Christel Baier, Marcus Größer, Frank Ciesinski
Model checking linear-time properties of probabilistic systems
In Manfred Droste and Werner Kuich and Heiko Vogler, eds., Handbook of weighted automata, Monographs in Theoretical Computer Science, 519--570. Springer, 2009

Details
Bibtex

KurzfassungAbstract
This chapter is about the verification of Markov decision processes (MDPs) which incorporate one of the fundamental models for reasoning about probabilistic and nondeterministic phenomena in reactive systems. MDPs have their roots in the field of operations research and are nowadays used in a wide variety of areas including verification, robotics, planning, controlling, reinforcement learning, economics and semantics of randomized systems. Furthermore, MDPs served as the basis for the introduction of probabilistic automata which are related to weighted automata. We describe the use of MDPs as an operational model for randomized systems, e.g., systems that employ randomized algorithms, multi-agent systems or systems with unreliable components or surroundings. In this context we outline the theory of verifying ω-regular properties of such operational models. As an integral part of this theory we use ω-automata, i.e., finite-state automata over finite alphabets that accept languages of infinite words. Additionally, basic concepts of important reduction techniques are sketched, namely partial order reduction of MDPs and quotient system reduction of the numerical problem that arises in the verification of MDPs. Furthermore we present several undecidability and decidability results for the controller synthesis problem for partially observable MDPs.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-01492-5_13.

@incollection{BGC2009,
  author    = {Christel Baier and Marcus Gr{\"{o}}{\ss}er and Frank Ciesinski},
  title     = {Model checking linear-time properties of probabilistic systems},
  editor    = {Manfred Droste and Werner Kuich and Heiko Vogler},
  booktitle = {Handbook of weighted automata},
  series    = {Monographs in Theoretical Computer Science},
  publisher = {Springer},
  year      = {2009},
  pages     = {519--570},
  doi       = {10.1007/978-3-642-01492-5_13}
}