Abstraction for model checking multi-agent systems

Clarke E, Grumberg O, Peled D. Model Checking. Cambridge: MIT Press, 2000

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

Fagin R, Halpern J, Moses Y, Vardi M. Reasoning about Knowledge. Cambridge: MIT Press, 1995

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

Su K, Sattar A, Luo X. Model checking temporal logics of knowledge via OBDDs. Computer Journal, 2007, 50(4): 403–420

McMillan K. Symbolic Model Checking. Norwell: Kluwer Academic Publishers, 1993

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)

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)

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

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

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

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

Clarke E M, Grumberg O, Long D E. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 1994, 16(5): 1512–1542

Penczek W, Lomuscio A. Verifying epistemic properties of multi-Agent systems via bounded model checking. Fundamenta Informaticae, 2003, 55(2): 167–185

Chaum D. The dining cryptographers problem: unconditional sender and recipient untraceability. Journal of Cryptology, 1988, 1(1): 65–75

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

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

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

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