Abstraction for model checking multi-agent systems

doi:10.1007/s11704-010-0358-y

Front Comput Sci Chin

2011, Vol. 5

Issue (1) : 14-25 https://doi.org/10.1007/s11704-010-0358-y

RESEARCH ARTICLE

Abstraction for model checking multi-agent systems

Conghua ZHOU(

), Bo SUN, Zhifeng LIU

School of Computer Science and Telecommunication Engineering, Jiangsu University, Zhenjiang 212013, China

Download: PDF(236 KB) HTML
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

Abstract

Model checking multi-agent systems (MAS) always suffers from the state explosion problem. In this paper we focus on an abstraction technique which is one of the major methods for overcoming this problem. For a multi-agent system, we present a novel abstraction procedure which reduces the state space by collapsing the global states in the system. The abstraction is automatically computed according to the property to be verified. The resulting abstract system simulates the concrete system, while the universal temporal epistemic properties are preserved. Our abstraction is an over-approximation. If some universal temporal epistemic property is not satisfied, then we need to identify spurious counterexamples. We further show how to reduce complex counterexamples to simple structures, i.e., paths and loops, such that the counterexamples can be checked and the abstraction can be refined efficiently. Finally, we illustrate the abstraction technique with a card game.

Keywords model checking abstraction refinement epistemic temporal logic

Corresponding Author(s): ZHOU Conghua,Email:chzhou@ujs.edu.cn

Issue Date: 05 March 2011

Cite this article:

Conghua ZHOU,Bo SUN,Zhifeng LIU. Abstraction for model checking multi-agent systems[J]. Front Comput Sci Chin, 2011, 5(1): 14-25.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-010-0358-y
https://academic.hep.com.cn/fcs/EN/Y2011/V5/I1/14

Fig.1 is tree like, is not

Fig.2 The parse tree for

Fig.3 Algorithm: generate tree like counterexamples for ACTLK

Fig.4 Algorithm: print the witness of

Fig.5 Initial abstraction for the concrete card game

Fig.6 Refinement of the initial abstraction

Tab.1 Compared with Cohen et al.’s approach

Tab.2 Abstraction for model checking the dining cryptographers protocol

1	Clarke E, Grumberg O, Peled D. Model Checking. Cambridge: MIT Press, 2000
2	Halpern J Y, Vardi M. Model checking vs. theorem proving: a manifesto. In: McCarthy J, Lifschitz V, eds. Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy . San Diego: Academic Press, 1991, 151–176
3	Fagin R, Halpern J, Moses Y, Vardi M. Reasoning about Knowledge. Cambridge: MIT Press, 1995
4	van der Hoek W, Wooldridge M. Model checking knowledge and time. In: Proceedings of 9th International SPIN Workshop on Model Checking of Software . 2002, 95–111
5	Su K, Sattar A, Luo X. Model checking temporal logics of knowledge via OBDDs. Computer Journal , 2007, 50(4): 403–420 doi: 10.1093/comjnl/bxm009
6	McMillan K. Symbolic Model Checking. Norwell: Kluwer Academic Publishers, 1993
7	Wu L, Su J, S K. Symbolic model checking knowledge and time in multi-agent system via extended mu-calculus. Chinese Journal of Computers , 2008, 31(02): 245–252 (in Chinese) doi: 10.3724/SP.J.1016.2008.00245
8	Luo X, Su K, Yang J. Bounded model checking for temporal epistemic logic in synchronous multi-agent systems. Journal of Software , 2006, 17(12): 2485–2498 (in Chinese) doi: 10.1360/jos172485
9	Biere A, Cimatti A, Clarke E, Zhu Y. Symbolic model checking without BDDs. In: Proceedings of 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems . 1999, 193–207 doi: 10.1007/3-540-49059-0_14
10	Peled D, Pnueli A. Proving partial order properties. Theoretical Computer Science , 1994, 126(2): 143–182 doi: 10.1016/0304-3975(94)90009-4
11	Emerson E, Sistla A. Symmetry and model checking. Formal Methods in System Design , 1996, 9(1-2): 105–131 doi: 10.1007/BF00625970
12	Wu L J, Su J S, Chen Q, Yang Z. Algorithm research on “on the fly” model checking temporal logics of knowledge in multi-agent systems. Journal of Computer Research and Development , 2006, 43(8): 1417–1424 doi: 10.1360/crad20060816
13	Clarke E M, Grumberg O, Long D E. Model checking and abstraction. ACM Transactions on Programming Languages and Systems , 1994, 16(5): 1512–1542 doi: 10.1145/186025.186051
14	Penczek W, Lomuscio A. Verifying epistemic properties of multi-Agent systems via bounded model checking. Fundamenta Informaticae , 2003, 55(2): 167–185
15	Chaum D. The dining cryptographers problem: unconditional sender and recipient untraceability. Journal of Cryptology , 1988, 1(1): 65–75 doi: 10.1007/BF00206326
16	Enea C, Dima C. Abstractions of multi-agent systems. In: Proceedings of 5th international Central and Eastern European conference on Multi-Agent Systems and Applications . 2007, 11–21
17	Cohen M, Dam M, Lomuscio A, Russo F. Abstraction in model checking multi-agent systems. In: Proceeding of 8th International Conference on Autonomous Agents and Multiagent Systems . 2009, 945–952
18	Clarke E M, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-guided abstraction refinement. In: Proceedings of 12th International Conference on Computer Aided Verification . 2000, 154–169 doi: 10.1007/10722167_15
19	Clarke E M, Jha S, Lu Y, Veith H. Tree-like counterexamples in model checking. In: Proceeding of 17th IEEE Symposium on Logic in Computer Science . 2002, 19–29 doi: 10.1109/LICS.2002.1029814

[1]	Yuanrui ZHANG, Frédéric MALLET, Yixiang CHEN. A verification framework for spatio-temporal consistency language with CCSL as a specification language[J]. Front. Comput. Sci., 2020, 14(1): 105-129.
[2]	Gaochang WU, Yipeng LI, Yuanhao HUANG, Yebin LIU. Joint view synthesis and disparity refinement for stereo matching[J]. Front. Comput. Sci., 2019, 13(6): 1337-1352.
[3]	Kazuhiro OGATA. A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions[J]. Front. Comput. Sci., 2019, 13(1): 51-72.
[4]	Anil Kumar KARNA, Yuting CHEN, Haibo YU, Hao ZHONG, Jianjun ZHAO. The role of model checking in software engineering[J]. Front. Comput. Sci., 2018, 12(4): 642-668.
[5]	Yu ZHOU, Nvqi ZHOU, Tingting HAN, Jiayi GU, Weigang WU. Probabilistic verification of hierarchical leader election protocol in dynamic systems[J]. Front. Comput. Sci., 2018, 12(4): 763-776.
[6]	Xueming WANG, Zechao LI, Jinhui TANG. Visual understanding by mining social media: recent advances and challenges[J]. Front. Comput. Sci., 2018, 12(3): 406-422.
[7]	Fei HE, Yuan GAO, Liangze YIN. Efficient software product-line model checking using induction and a SAT solver[J]. Front. Comput. Sci., 2018, 12(2): 264-279.
[8]	Xuexia ZHONG,Guorui FENG,Jian WANG,Wenfei WANG,Wen SI. A novel adaptive image zooming scheme via weighted least-squares estimation[J]. Front. Comput. Sci., 2015, 9(5): 703-712.
[9]	Laixiang SHAN,Xiaomin DU,Zheng QIN. Efficient approach of translating LTL formulae into Büchi automata[J]. Front. Comput. Sci., 2015, 9(4): 511-523.
[10]	Luxi CHEN,Linpeng HUANG,Chen LI,Tao ZAN. Integrating behavior analysis into architectural modeling[J]. Front. Comput. Sci., 2015, 9(1): 15-33.
[11]	Yuanjie SI, Jun SUN, Yang LIU, Jin Song DONG, Jun PANG, Shao Jie ZHANG, Xiaohu YANG. Model checking with fairness assumptions using PAT[J]. Front. Comput. Sci., 2014, 8(1): 1-16.
[12]	Cuiyun HU, Xinjun MAO, Mengjun LI, Zhi ZHU. Organization-based agent-oriented programming: model, mechanisms, and language[J]. Front. Comput. Sci., 2014, 8(1): 33-51.
[13]	Savas KONUR. A survey on temporal logics for specifying and verifying real-time systems[J]. Front. Comput. Sci., 2013, 7(3): 370-403.
[14]	Bo WANG, Zhenjiang HU, Qiang SUN, Haiyan ZHAO, Yingfei XIONG, Wei ZHANG, Hong MEI. Supporting feature model refinement with updatable view[J]. Front Comput Sci, 2013, 7(2): 257-271.
[15]	Anh Tuan LUU, Jun SUN, Yang LIU, Jin Song DONG, Xiaohong LI, Thanh Tho QUAN. SeVe: automatic tool for verification of security protocols[J]. Front Comput Sci, 2012, 6(1): 57-75.

Viewed

Full text

Abstract

Cited

Shared

Discussed