Abstraction in model checking multi-agent systems

ABSTRACT

We present an abstraction technique for multi-agent systems preserving temporal-epistemic specifications. We abstract a multi-agent system, defined in the interpreted systems framework, by collapsing the local states and actions of each agent in the system. We show that the resulting abstract system simulates the concrete system, from which we obtain a preservation theorem: If a temporal-epistemic specification holds on the abstract system, the specification also holds on the concrete one. In principle this permits us to model check the abstract system rather than the concrete one, thereby saving time and space in the verification step. We illustrate the abstraction technique with two examples. The first example, a card game, illustrates the potential savings in the cost of model checking a typical MAS scenario. In the second example, the abstraction technique is used to verify a communication protocol with an arbitrarily large data domain.

REFERENCES

• 1: T. Ball and S. K. Rajamani. Boolean programs: A model and process for software analysis. MSR Technical Report 2000-14. 2000.
• 2: Rafael H. Bordini , Michael Fisher , Carmen Pardavila , Michael Wooldridge, Model checking agentspeak, Proceedings of the second international joint conference on Autonomous agents and multiagent systems, July 14-18, 2003, Melbourne, Australia [doi>10.1145/860575.860641]
• 3: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 4: Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
• 5: Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-Guided Abstraction Refinement, Proceedings of the 12th International Conference on Computer Aided Verification, p.154-169, July 15-19, 2000
• 6: Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1512-1542, Sept. 1994 [doi>10.1145/186025.186051]
• 7: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 8: Satyaki Das , David L. Dill, Successive Approximation of Abstract Transition Relations, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.51, June 16-19, 2001
• 9: Francien Dechesne , Simona Orzan , Yanjing Wang, Refinement of Kripke Models for Dynamics, Proceedings of the 5th international colloquium on Theoretical Aspects of Computing, p.111-125, September 01-03, 2008, Istanbul, Turkey [doi>10.1007/978-3-540-85762-4_8]
• 10: E. A. Emerson and E. M. Clarke. Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2(3):241--266, 1982.
• 11: Constantin Enea , Catalin Dima, Abstractions of Multi-agent Systems, Proceedings of the 5th international Central and Eastern European conference on Multi-Agent Systems and Applications V, September 25-27, 2007, Leipzig, Germany [doi>10.1007/978-3-540-75254-7_2]
• 12: Ronald Fagin , Joseph Y. Halpern , Moshe Y. Vardi , Yoram Moses, Reasoning about knowledge, MIT Press, Cambridge, MA, 1995
• 13: P. Gammie and R. van der Meyden. MCK: Model checking the logic of knowledge. In CAV'04, volume 3114 of LNCS, pages 479--483. Springer-Verlag, 2004.
• 14: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 15: Robert P. Kurshan, Computer-aided verification of coordinating processes: the automata-theoretic approach, Princeton University Press, Princeton, NJ, 1994
• 16: W. Nabialek, A. Niewiadomski, W. Penczek, A. Pólrola, and M. Szreter. Verics 2004: A model checker for real time and multi-agent systems. In CS&P'04, volume 170 of Informatik-Berichte, pages 88--99. Humboldt University, 2004.
• 17: Wojciech Penczek , Alessio Lomuscio, Verifying epistemic properties of multi-agent systems via bounded model checking, Fundamenta Informaticae, v.55 n.2, p.167-185, August 2002
• 18: F. Raimondi and A. Lomuscio. Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams. Journal of Applied Logic, 5(2):235--251, 2007.
• 19: Computationally Grounded Theories of Agency, Proceedings of the Fourth International Conference on MultiAgent Systems (ICMAS-2000), p.13, July 10-12, 2000
• 20: Michael Wooldridge , Michael Fisher , Marc-Philippe Huget , Simon Parsons, Model checking multi-agent systems with MABLE, Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2, July 15-19, 2002, Bologna, Italy [doi>10.1145/544862.544965]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.4 Knowledge Representation Formalisms and Methods

General Terms:
Theory, Verification

Keywords:
abstraction, epistemic logic, model checking