Model Checking Probabilistic Systems

Christel BaierChristel Baier, Luca de AlfaroLuca de Alfaro, Vojtech ForejtVojtech Forejt, Marta KwiatkowskaMarta Kwiatkowska

DOI Link

Christel Baier, Luca de Alfaro, Vojtech Forejt, Marta Kwiatkowska
Model Checking Probabilistic Systems
In Edmund M. Clarke and Thomas A. Henzinger and Helmut Veith and Roderick Bloem, eds., Handbook of Model Checking, 963--999. Springer, 2018

Details
Bibtex

KurzfassungAbstract
The model-checking approach was originally formulated for verifying qualitative properties of systems, for example safety and liveness (see Chap. 2), and subsequently extended to also handle quantitative features, such as real time (see Chap. 29), continuous flows (see Chap. 30), as well as stochastic phenomena, where system evolution is governed by a given probability distribution. Probabilistic model checking aims to establish the correctness of probabilistic system models against quantitative probabilistic specifications, such as those capable of expressing, for example, the probability of an unsafe event occurring, expected time to termination, or expected power consumption in the start-up phase. In this chapter, we present the foundations of probabilistic model checking, focusing on finite-state Markov decision processes as models and quantitative properties expressed in probabilistic temporal logic. Markov decision processes can be thought of as a probabilistic variant of labelled transition systems in the following sense: transitions are labelled with actions, which can be chosen nondeterministically, and successor states for the chosen action are specified by means of discrete probabilistic distributions, thus specifying the probability of transiting to each successor state. To reason about expectations, we additionally annotate Markov decision processes with quantitative costs, which are incurred upon taking the selected action from a given state. Quantitative properties are expressed as formulas of the probabilistic computation tree logic (PCTL) or using linear temporal logic (LTL). We summarise the main model-checking algorithms for both PCTL and LTL, and illustrate their working through examples. The chapter ends with a brief overview of extensions to more expressive models and temporal logics, existing probabilistic model-checking tool support, and main application domains.
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-319-10575-8_28.

@incollection{BAFK2018,
  author    = {Christel Baier and Luca de Alfaro and Vojtech Forejt and Marta
               Kwiatkowska},
  title     = {Model Checking Probabilistic Systems},
  editor    = {Edmund M. Clarke and Thomas A. Henzinger and Helmut Veith and
               Roderick Bloem},
  booktitle = {Handbook of Model Checking},
  publisher = {Springer},
  year      = {2018},
  pages     = {963--999},
  doi       = {10.1007/978-3-319-10575-8_28}
}