Model checking knowledge, strategies, and games in multi-agent systems

ABSTRACT

We present an OBDD-based methodology for verifying time, knowledge, and strategies in multi-agent systems specified by the formalism of interpreted systems. To this end, we investigate the interpretation of ATL and epistemic formulae in various classes of interpreted systems, we present model checking algorithms and their implementation, and report experimental results.

REFERENCES

• 1: T. Agotnes. Action and knowledge in Alternating-time Temporal Logic. Synthese, 2005. Special issue on Knowledge, Rationality and Action.
• 2: Rajeev Alur , Thomas A. Henzinger , Freddy Y. C. Mang , Shaz Qadeer , Sriram K. Rajamani , Serdar Tasiran, MOCHA: Modularity in Model Checking, Proceedings of the 10th International Conference on Computer Aided Verification, p.521-525, June 28-July 02, 1998
• 3: Rajeev Alur , Thomas A. Henzinger , Orna Kupferman, Alternating-time temporal logic, Journal of the ACM (JACM), v.49 n.5, p.672-713, September 2002 [doi>10.1145/585265.585270]
• 4: 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]
• 5: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 6: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 7: Ronald Fagin , Joseph Y. Halpern , Moshe Y. Vardi , Yoram Moses, Reasoning about knowledge, MIT Press, Cambridge, MA, 1995
• 8: P. Gammie and R. van der Meyden. MCK: Model checking the logic of knowledge. In Proceedings of 16th International Conference on Computer Aided Verification (CAV'04), volume 3114 of LNCS, pages 479--483. Springer-Verlag, 2004.
• 9: V. Goranko and W. Jamroga. Comparing semantics for logics of multi-agent systems. Synthese, 139(2):241--280, 2004.
• 10: Wiebe van der Hoek , Wojciech Jamroga , Michael Wooldridge, A logic for strategic reasoning, Proceedings of the fourth international joint conference on Autonomous agents and multiagent systems, July 25-29, 2005, The Netherlands [doi>10.1145/1082473.1082497]
• 11: Wiebe van der Hoek , Michael Wooldridge, Tractable multiagent planning for epistemic goals, Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 3, July 15-19, 2002, Bologna, Italy [doi>10.1145/545056.545095]
• 12: W. Jamroga. Some remarks on alternating temporal epistemic logic. In B. Dunin-Kȩplicz and R. Verbrugge, editors, Proceedings of the International Workshop on Formal Approaches to Multi-Agent Systems (FAMAS'03), pages 133--140, 2004.
• 13: W. Jamroga. Using Multiple Models of Reality. On Agents who Know how to Play Safer. PhD thesis, University of Twente, Enschede, The Netherlands, 2004.
• 14: Wojciech Jamroga , Wiebe van der Hoek, Agents that Know How to Play, Fundamenta Informaticae, v.63 n.2-3, p.185-219, April 2004
• 15: G. Jonker. Feasible strategies in alternating-time temporal epistemic logic. Master's thesis, University of Utrech, The Netherlands, 2003.
• 16: M. Kacprzak and W. Penczek. A SAT-based approach to unbounded model checking for alternating-time temporal epistemic logic. Synthese, 142:203--227, 2004.
• 17: A. Lomuscio. Knowledge Sharing among Ideal Agents. PhD thesis, School of Computer Science, University of Birmingham, Birmingham, UK, June 1999.
• 18: R. C. Moore. A formal theory of knowledge and action. In J. Allen, J. Hendler, and A. Tate, editors, Readings in Planning, pages 480--519. Kaufmann, San Mateo, CA, 1990.
• 19: 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 Proceedings of the International Workshop on Concurrency, Specification and Programming (CS&P'04), volume 170 of Informatik-Berichte, pages 88--99. Humboldt University, 2004.
• 20: S. Otterloo, W. van der Hoek, and M. Wooldridge. Knowledge as strategic ability. ENCTS, 85(2):1--23, 2003.
• 21: F. Raimondi and A. Lomuscio. MCMAS - A tool for verification of multi-agent systems. http://www.cs.ucl.ac.uk/staff/f.raimondi/MCMAS/.
• 22: F. Raimondi and A. Lomuscio. Automatic verification of multi-agent systems by model checking via OBDDs. Journal of Applied Logic, 2005. To appear in Special issue on Logic-based agent verification.
• 23: P. Y. Schobbens. Alternating-time logic with imperfect recall. In International workshop on Logic and Communication in Multi-Agent Systems (LCMAS03), volume 85(2), pages 1--12, 2004.
• 24: F. Somenzi. CUDD: CU decision diagram package - release 2.4.0. http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html, 2005.
• 25: 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

General Terms:
Algorithms, Theory, Verification

Keywords:
ATL, model checking multi-agent systems