Model Checking Probabilistic Systems
Model Checking Probabilistic Systems
复制标题
模型检查概率系统
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
M. Kwiatkowska
中科院分区：
文献类型：
--
作者：
C. Baier;L. D. Alfaro;Vojtěch Forejt;M. Kwiatkowska
模型检查方法最初是为验证系统的定性属性而制定的，例如安全性和活性(见第二章)。2)，并随后扩展到也处理定量特征，例如实时(见第二章)。29)、连续流动(见第二章)。30)，以及随机现象，其中系统演化受给定的概率分布支配。概率模型检验的目的是对照定量概率规范来建立概率系统模型的正确性，所述定量概率规范例如能够表达不安全事件发生的概率、预期终止时间或启动阶段的预期功耗。在这一章中，我们介绍了概率模型检验的基础，重点介绍了有限状态马尔可夫决策过程作为模型和用概率时序逻辑表示的定量性质。马尔可夫决策过程在以下意义上可以被认为是标签转移系统的概率变体：转移用动作来标记，这些动作可以不确定地选择，所选动作的后继状态通过离散概率分布来指定，从而指定转移到每个后继状态的概率。为了推断预期，我们还使用定量成本来注释马尔可夫决策过程，这些成本是在从给定状态采取所选操作时发生的。定量属性被表示为概率计算树逻辑(PCTL)或使用线性时序逻辑(LTL)的公式。我们总结了PCTL和LTL的主要模型检测算法，并通过实例说明了它们的工作原理。本章最后简要概述了对更具表现力的模型和时序逻辑的扩展、现有的概率模型检测工具支持以及主要应用领域。
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.
DOI：
10.1007/978-3-642-39799-8_37
发表时间：
2013-04
期刊：
--
影响因子：
--
作者：
K. Chatterjee;Andreas Gaiser;Jan Křetínský
通讯作者：
K. Chatterjee;Andreas Gaiser;Jan Křetínský
影响因子：
1.1
作者：
Ciocchetta, Federica;Hillston, Jane
通讯作者：
Hillston, Jane
影响因子：
1.1
作者：
Heath, John;Kwiatkowska, Marta;Tymchyshyn, Oksana
通讯作者：
Tymchyshyn, Oksana