Probabilistic Model Checking

BAIER, Christel, Luca DE ALFARO, Vojtěch FOREJT a Marta KWIATKOWSKA. Probabilistic Model Checking. In Handbook of Model Checking. Germany: Springer, 2018, 39 s. ISBN 978-3-319-10575-8.

Základní údaje

Originální název

Probabilistic Model Checking

Autoři

BAIER, Christel, Luca DE ALFARO, Vojtěch FOREJT a Marta KWIATKOWSKA

Vydání

Germany, Handbook of Model Checking, 39 s. 2018

Nakladatel

Springer

---

Další údaje

Jazyk

angličtina

Typ výsledku

Kapitola resp. kapitoly v odborné knize

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-10575-8

Klíčová slova anglicky

model checking; ltl; pctl

Štítky

topvydavatel

---

Anotace

V originále

The model-checking approach was originally formulated for verifying qualitative properties of systems, for example safety and liveness, and subsequently extended to also handle quantitative features, such as real-time, continuous flows, 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, e.g., 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.