利用分层实现高效的 CSL 模型检验
计算机科学中的逻辑
2015-07-01 v3
摘要
对于连续时间马尔可夫链，Aziz、Sanwal、Singhal 和 Brayton 于 1996 年引入并证明了关于连续时间随机逻辑 (CSL) 的模型检验问题是可判定的。他们的证明可转化为一个复杂度比指数级更差的近似算法。2000 年，Baier、Haverkort、Hermanns 和 Katoen 针对仅允许二元 until 算子的子逻辑，提出了一个高效的多项式时间近似算法。本文中，我们为完整的 CSL 提出了这样一个高效的多项式时间近似算法。我们方法的关键是针对待检验的 CSL 性质，引入分层 CTMC 的概念。在分层 CTMC 上，满足一个 CSL 路径公式的概率可通过瞬态分析在多项式时间内近似（利用均匀化）。我们给出了将任意 CTMC 转化为一个等价的分层 CTMC 的保测度、线性时间和空间的变换。这使得本工作成为一个广泛适用的完整 CSL 模型检验器的核心。最近，Aziz 等人的判定算法被证明仅对分层 CTMC 有效。作为额外贡献，我们的保测度变换可用于确保一般 CTMC 的可判定性。
引用
@article{arxiv.1104.4983,
title = {Efficient CSL Model Checking Using Stratification},
author = {Lijun Zhang and David N. Jansen and Flemming Nielson and Holger Hermanns},
journal= {arXiv preprint arXiv:1104.4983},
year = {2015}
}
备注
18 pages, preprint for LMCS. An extended abstract appeared in ICALP 2011