Další formáty:
BibTeX
LaTeX
RIS
@inbook{1378306, author = {Baier, Christel and de Alfaro, Luca and Forejt, Vojtěch and Kwiatkowska, Marta}, address = {Germany}, booktitle = {Handbook of Model Checking}, keywords = {model checking; ltl; pctl}, language = {eng}, location = {Germany}, isbn = {978-3-319-10575-8}, publisher = {Springer}, title = {Probabilistic Model Checking}, year = {2018} }
TY - CHAP ID - 1378306 AU - Baier, Christel - de Alfaro, Luca - Forejt, Vojtěch - Kwiatkowska, Marta PY - 2018 TI - Probabilistic Model Checking PB - Springer CY - Germany SN - 9783319105758 KW - model checking KW - ltl KW - pctl N2 - 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. ER -
BAIER, Christel, Luca DE ALFARO, Vojtěch FOREJT a Marta KWIATKOWSKA. Probabilistic Model Checking. In \textit{Handbook of Model Checking}. Germany: Springer, 2018, 39 s. ISBN~978-3-319-10575-8.
|