基于分层的高效CSL模型检验
Efficient CSL Model Checking Using Stratification
摘要：
对于连续时间马尔可夫链，关于连续时间随机逻辑（CSL）的模型检验问题已经被Aziz，Sanwal，Singhal和Brayton在1996年引入并证明是可判定的。他们的证明可以转化为比指数复杂度更差的近似算法。2000年，Baier，Haverkort，Hermanns和Katoen提出了一种有效的多项式时间近似算法，用于只允许二进制直到的子逻辑。在本文中，我们提出了这样一个有效的多项式时间近似算法的充分CSL。我们的方法的关键是分层CTMC的概念相对于CSL属性进行检查。在分层CTMC上，满足CSL路径公式的概率可以通过多项式时间的瞬态分析来近似（使用均匀化）。我们提出了一个措施保持，线性时间和空间变换的任何CTMC到一个等价的，分层的。这使得目前的工作的核心广泛适用的CSL模型检查。最近，Aziz等人的决策算法被证明仅适用于分层CTMC。作为一个额外的贡献，我们的测量保持转换可以用来确保一般CTMC的可判定性。
英文摘要：
For continuous-time Markov chains, the model-checking problem with respect to continuous-time stochastic logic (CSL) has been introduced and shown to be decidable by Aziz, Sanwal, Singhal and Brayton in 1996. Their proof can be turned into an approximation algorithm with worse than exponential complexity. In 2000, Baier, Haverkort, Hermanns and Katoen presented an efficient polynomial-time approximation algorithm for the sublogic in which only binary until is allowed. In this paper, we propose such an efficient polynomial-time approximation algorithm for full CSL. The key to our method is the notion of stratified CTMCs with respect to the CSL property to be checked. On a stratified CTMC, the probability to satisfy a CSL path formula can be approximated by a transient analysis in polynomial time (using uniformization). We present a measure-preserving, linear-time and -space transformation of any CTMC into an equivalent, stratified one. This makes the present work the centerpiece of a broadly applicable full CSL model checker. Recently, the decision algorithm by Aziz et al. was shown to work only for stratified CTMCs. As an additional contribution, our measure-preserving transformation can be used to ensure the decidability for general CTMCs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
