Symbolic Model Checking of Stochastic Systems: Theory and Implementation
Symbolic Model Checking of Stochastic Systems: Theory and Implementation
复制标题
随机系统的符号模型检查：理论与实现
作者：
M. Kuntz;Markus Siegle
本文提出了 IM-SPDL，它是模态逻辑 PDL 的随机扩展，支持复杂性能和可靠性要求的规范。该逻辑通过扩展随机标记转换系统（ESLTS）进行解释，即包含立即转换和马尔可夫转换的转换系统。我们定义了新逻辑的语法和语义，并表明 IM-SPDL 提供了强大的方法来指定具有时序限制的基于路径的属性。一般来说，路径可以用正则表达式来表征，也称为程序，其中程序的可执行性可能取决于测试公式的有效性。对于 IM-SPDL 时间限制路径公式的模型检查，根据需求构建了确定性程序自动机。然后，建立了该自动机和 ESLTS 之间的产品转换系统，并随后将其转换为连续时间马尔可夫链 (CTMC)，并对其进行数值分析。论文给出的实证结果表明，模型检验IM-SPDL在实践中可以有效地实现。
This paper presents IM-SPDL, a stochastic extension of the modal logic PDL, which supports the specification of complex performance and dependability requirements. The logic is interpreted over extended stochastic labelled transition systems (ESLTS), i.e. transition systems containing both immediate and Markovian transitions. We define the syntax and semantics of the new logic and show that IM-SPDL provides powerful means to specify path-based properties with timing restrictions. In general, paths can be characterised by regular expressions, also called programs, where the executability of a program may depend on the validity of test formulae. For the model checking of IM-SPDL time-bounded path formulae, a deterministic program automaton is constructed from the requirement. Afterwards the product transition system between this automaton and the ESLTS is built and subsequently transformed into a continuous time Markov Chain (CTMC) on which numerical analysis is performed. Empirical results given in the paper show that model checking IM-SPDL can be realised efficiently in practice.