Verifying pCTL Model Checking
Verifying pCTL Model Checking
复制标题
验证 pCTL 模型检查
DOI：
10.1007/978-3-642-28756-5_24
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Tobias Nipkow
中科院分区：
文献类型：
--
作者：
Johannes Hölzl;Tobias Nipkow
像PRISM这样的概率模型检查器根据离散时间马尔可夫链来检查概率CTL(PCTL)公式的可满足性。我们在Isabelle/HOL中证明了其基本算法的可靠性和完备性。我们定义了由转移矩阵给出的马氏链，并在路径集上形式化了相应的概率度量。PCTL公式的形式化包括无界累积奖励。
Probabilistic model checkers like PRISM check the satisfiability of probabilistic CTL (pCTL) formulas against discrete-time Markov chains. We prove soundness and completeness of their underlying algorithm in Isabelle/HOL. We define Markov chains given by a transition matrix and formalize the corresponding probability measure on sets of paths. The formalization of pCTL formulas includes unbounded cumulated rewards.
登录
查看更多内容
用于 LTL 模型检查的 Büchi 自动机构建在 Isabelle/HOL 得到验证
影响因子：
0.8
作者：
A. Schimpf;Stephan Merz;J. Smaus
通讯作者：
J. Smaus
表示为函数的矩阵的高斯约当消元法
DOI：
--
发表时间：
2011
期刊：
Arch. Formal Proofs
影响因子：
--
作者：
T. Nipkow
通讯作者：
T. Nipkow
HOL 中有限状态离散时间马尔可夫链的形式化
DOI：
--
发表时间：
2011
期刊：
Automated Technology for Verification and Analysis
影响因子：
--
作者：
Liya Liu;O. Hasan;S. Tahar
通讯作者：
S. Tahar
匿名、信息和机器辅助证明
DOI：
--
发表时间：
2010
期刊：
影响因子：
--
作者：
A. R. Coble
通讯作者：
A. R. Coble
《Isabelle/HOL》中的测度论三章
DOI：
10.1007/978-3-642-22863-6_12
发表时间：
2011
期刊：
影响因子：
--
作者：
Johannes Hölzl;Armin Heller
通讯作者：
Armin Heller