Model checking linear-time properties of probabilistic systems
From International Center for Computational Logic
Model checking linear-time properties of probabilistic systems
Christel BaierChristel Baier, Marcus GrößerMarcus Größer, Frank CiesinskiFrank Ciesinski
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
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
- 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
@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}
}