Abstraction for model checking multi-agent systems

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

References

[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

[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)

[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)

[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

[10] Peled D, Pnueli A. Proving partial order properties. Theoretical Computer Science, 1994, 126(2): 143–182

[11] Emerson E, Sistla A. Symmetry and model checking. Formal Methods in System Design, 1996, 9(1-2): 105–131

[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

[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

[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

[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

[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

Acknowledgements

This work was supported by the National Natural Science Foundation of China (Grant No. 60773049, 61003288), the People with Ability Foundation of Jiangsu University (No. 07JDG014), the Fundamental Research Project of the Natural Science in Colleges of Jiangsu Province (No. 08KJD520015), and the Ph.D. Programs Foundation of Ministry of Education of China (No. 20093227110005).

RIGHTS & PERMISSIONS

2014 Higher Education Press and Springer-Verlag Berlin Heidelberg