概率时态认知逻辑模型检测中三值抽象技术的研究

doi:10.3969/j.issn.0372-2112.2012.10.025

PDF(759 KB)

电子学报 ›› 2012, Vol. 40 ›› Issue (10) : 2052-2061. DOI: 10.3969/j.issn.0372-2112.2012.10.025

学术论文

概率时态认知逻辑模型检测中三值抽象技术的研究

周从华, 孙博, 刘志锋, 葛云

作者信息 +

Three-Valued Abstraction for Model Checking the Probabilistic Temporal Logic of Knowledge

ZHOU Cong-hua, SUN Bo, LIU Zhi-feng, GE Yun

Author information +

文章历史 +

摘要

为缓解概率时态认知逻辑模型检测中的状态空间爆炸问题,提出了概率时态认知逻辑的三值抽象技术.具体研究内容包括:定义抽象模型及模型上概率时态认知逻辑的三值语义,依据状态空间等价划分建立初始抽象模型,并证明抽象技术对概率时态认知逻辑的满足性保持关系;提出概率时态认知逻辑模型检测算法;依据初始模型检测的结果,给出利用最小证据和最小反例引导的抽象系统的求精过程.最后通过Dining Cryptographer协议说明了抽象技术的应用,及其在约简系统状态空间方面的效果.

Abstract

In order to overcome the state explosion problem in model checking the probabilistic temporal logic of knowledge,a three-valued abstraction is proposed.Our work includes three parts:first the three-value semantics of the probabilistic temporal logic of knowledge is defined on the abstract model,and the initial abstract model is build according to the equivalence partition of state space,and the preservation of satisfaction under the abstraction is proved;second the model checking algorithm of the probabilistic temporal logic of knowledge is proposed;third how to refine the abstraction by the minimal witnesses and counterexamples generated in model checking is shown.Finally,the abstraction is applied in model checking the Dining Cryptographer protocols.

导出引用

周从华, 孙博, 刘志锋, 葛云. 概率时态认知逻辑模型检测中三值抽象技术的研究[J]. 电子学报, 2012, 40(10): 2052-2061. https://doi.org/10.3969/j.issn.0372-2112.2012.10.025

ZHOU Cong-hua, SUN Bo, LIU Zhi-feng, GE Yun. Three-Valued Abstraction for Model Checking the Probabilistic Temporal Logic of Knowledge[J]. Acta Electronica Sinica, 2012, 40(10): 2052-2061. https://doi.org/10.3969/j.issn.0372-2112.2012.10.025

中图分类号： TP301

参考文献

[1] E M Clarke,O Grumberg,D Peled.Model Checking[M].MIT Press,1999.
[2] 林惠民,张文辉.模型检测:理论、方法与应用[J].电子学报,2002,30 (12A):1907-1912. Lin Huimin,Zhang Wenhui.Model checking:theories,techniques and applications[J].Acta Electronica Sinica,2002,30(12A):9-14(in Chinese).
[3] N Ferreira,M Fisher,W Hoek.Practical Reasoning for Uncertain Agents[J].Lecture Notes in Computer Science,2004,3229:82-94.
[4] Z Cao.Model checking for epistemic and temporal properties of uncertain agents[J].Lecture Notes in Computer Science,2006,4088:46-58.
[5] R E Bryant.Graph-based algorithms for boolean function manipulation[J].IEEE Transaction on Computers,1986,35(8):687-691.
[6] P Wolper,P Godefroid.Partial order methods for temporal verification[J].Lecture Notes in Computer Science,1993,715:233-246.
[7] E A Emerson,A P Sistla.Symmetry and model checking[J].Formal Methods in System Design,1996,9(1):105-131.
[8] E M Clarke,O Grumberg,D E Long.Model checking and abstraction[J].ACM Transactions on Programming Languages and Systems,1992,16 (5):1512-1542.
[9] 屈婉霞,李暾,郭阳,杨晓东.谓词抽象技术研究[J].软件学报,2008,19(01):27-38. Qu Wanxia,Li Tun,Guo Yang,Yang Xiaodong.Advances in Predicate Abstraction[J]. Journal of Software,2008,19(01):27-38.(in Chinese)
[10] O Grumberg.3-Valued Abstraction for (Bounded) Model Checking[J].Lecture Notes in Computer Science,2009,5799:21-21.
[11] E M Clarke,O Grumberg,S Jha,Y Lu,H Veith.Counterexample-guided abstraction refinement for symbolic model checking[J].Journal of the ACM,2003,50(3):752-794.
[12] J P Katoen,D Klink,M Leucker,V Wolf.Three-valued abstraction for probabilistic systems[J].J Log Algebr Program,2012,81(4):356-389.
[13] D Chaum.The dining cryptographers problem:unconditional sender and recipient untraceability[J].J Cryptology,1988,1(1):65-75.
[14] R Meyden,K Su.Symbolic model checking the knowledge of the dining cryptographers [A].In Proc.17th IEEE Computer Security Foundations Workshop [A].IEEE Computer Soci-ety,2004.280-291.
[15] 骆翔宇,苏开乐,杨晋吉.有界模型检测同步多智体系统的时态认知逻辑[J].软件学报,2006,17(12):2485-2498. Luo Xiangyu,Su Kaile,Yang Jinji.Bounded model checking for temporal epistemic logic in synchronous multi-agent systems[J].Journal of Software,2006,17(12):2485-2498.(in Chinese)