基于广义可能性测度的定量计算树逻辑模型检测
计算机科学中的逻辑
2014-09-24 v1
摘要
本文研究了广义可能主义计算树逻辑模型检测，这是对 Y.Li、Y.Li 和 Z.Ma (2014) 引入的可能主义计算树逻辑模型检测的扩展。系统由广义可能主义 Kripke 结构（简称 GPKS）建模，待验证属性由广义可能主义计算树逻辑（简称 GPoCTL）公式指定。基于广义可能性测度和广义必然性测度，讨论了广义可能主义计算树逻辑模型检测的方法，并详细展示了相应算法及其复杂度。此外，给出了 (2013) 年引入的 PoCTL 与 GPoCTL 之间的比较。最后，通过一个恒温器示例说明了 GPoCTL 模型检测方法。
引用
@article{arxiv.1409.6466,
title = {Quantitative Computation Tree Logic Model Checking Based on Generalized Possibility Measures},
author = {Yongming Li and Zhanyou Ma},
journal= {arXiv preprint arXiv:1409.6466},
year = {2014}
}