Model-checking algorithms for continuous-time Markov chains
Model-checking algorithms for continuous-time Markov chains
复制标题
DOI：
10.1109/tse.2003.1205180
复制
发表时间：
2003-06-01
影响因子：
7.4
通讯作者：
Katoen, JP
中科院分区：
文献类型：
--
作者：
Baier, C;Haverkort, B;Katoen, JP
连续时间马尔可夫链（CTMC）已被广泛用于确定系统性能和可靠性特征。他们的分析通常涉及稳态和瞬态状态概率的计算。本文介绍了用于表达CTMC上实时概率属性的分支时间逻辑，并介绍了该逻辑检查算法的近似模型。逻辑是Aziz等人的连续随机逻辑CSL的扩展，它包含一个时间限制的，直到运算符在路径上表达概率的正时属性以及表达稳态概率的操作员。我们表明，此逻辑的模型检查问题将减少到线性方程系统（无限制直至和稳态操作员）和Volterra积分方程系统（用于时间到达）。然后，我们证明了检查模型的时间限制的问题，直到可以将属性降低到计算CTMC的瞬态状态概率的问题为止。这允许通过有效的CTMC（例如均匀化）进行瞬时分析来验证概率的时序特性。最后，我们表明，汇总汇总CTMC的众所周知概念的变体等效性（双仿真）保留了逻辑中AFT公式的有效性。
Continuous-time Markov chains (CTMCs) have been widely used to determine system performance and dependability characteristics. Their analysis most often concerns the computation of steady-state and transient-state probabilities. This paper introduces a branching temporal logic for expressing real-time probabilistic properties on CTMCs and presents approximate model checking algorithms for this logic. The logic, an extension of the continuous stochastic logic CSL of Aziz et al., Contains a time-bounded until operator to express probabilistic timing properties over paths as well as an operator to express steady-state probabilities. We show that the model checking problem for this logic reduces to a system of linear equations (for unbounded until and the steady-state operator) and a Volterra integral equation system (for time-bounded until). We then show that the problem of model-checking time-bounded until properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allow's the verification of probabilistic timing properties by efficient techniques for transient analysis for CTMCs such as uniformization. Finally, we show that a variant of lumping equivalence (bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of aft formulas in the logic.