Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking

• Autorzy: Penczek W. , Lomuscio A.
• Języki publikacji: EN

Abstrakty

EN

We present a framework for verifying temporal and epistemic properties of multi-agent systems by means of bounded model checking. We use interpreted systems as underlying semantics. We give details of the proposed technique, and show how it can be applied to the ``attacking generals problem'', a typical example of coordination in multi-agent systems.

Słowa kluczowe

EN

Computation Tree Logic Knowledge (CTLK); modal logic; multi-agent systems

• Wydawca: Polskie Towarzystwo Matematyczne
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2003
• Tom: Vol. 55, nr 2
• Strony: 167--185
• Opis fizyczny: bibliogr.28 poz.

Twórcy

autor

Penczek W.

autor

Lomuscio A.

• Institute of Computer Science, Polish Academy of Science, Ordona 21, 01-237 Warsaw, Poland,

Bibliografia

• [1] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. of TACAS’99, volume 1579 of LNCS, pages 193-207. Springer-Verlag, 1999.
• [2] M. E. Bratman. Intentions, Plans, and Practical Reason. Harvard University Press: Cambridge, MA, 1987.
• [3] E. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19(1):7-34, 2001.
• [4] E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
• [5] E. A. Emerson. Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter Temporal and Modal Logic, pages 995-1067. Elsevier, 1990.
• [6] 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.
• [7] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, 1995.
• [8] R. Fagin, J. Y. Halpern, and M. Y. Vardi. What can machines know? On the properties of knowledge in distributed systems. Journal of the ACM, 39(2):328-376, Apr. 1992.
• [9] J. Halpern, R. Meyden, and M. Y. Vardi. Complete axiomatisations for reasoning about knowledge and time. SIAM Journal on Computing, 2003. To Appear.
• [10] J. Halpern and Y. Moses. Knowledge and common knowledge in a distributed environment. Journal of the ACM, 37(3):549-587, 1990. A preliminary version appeared in Proc. 3rd ACM Symposium on Principles of Distributed Computing, 1984.
• [11] W. van der Hoek and M. Wooldridge. Model checking knowledge and time. In Proc. of the 9th Int. SPIN Workshop (SPIN’02), volume 2318 of LNCS, pages 95-111. Springer-Verlag, 2002.
• [12] W. van der Hoek and M. Wooldridge. Tractable multiagent planning for epistemic goals. In Proc. of the 1st Int. Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS’02), July 2002. to appear.
• [13] R. van der Meyden and H. Shilov. Model checking knowledge and time in systems with perfect knowledge. In Proceedings of Proc. of FST&TCS, volume 1738 of Lecture Notes in Computer Science, pages 432-445, Hyderabad, India, 1999.
• [14] ISO/IEC 9074(E), Estelle - a formal description technique based on an extended state-transition model. International Standards Organization, 1997.
• [15] B. van Linder, W. van der Hoek, and J.-J. Meyer. Seeing is believing, and so are hearing and jumping. Journal of Logic, Language, and Information, 6(1):33-61, 1997.
• [16] A. Lomuscio, T. Łasica, and W. Penczek. Bounded model checking for interpreted systems: preliminary experimental results. In M. Hinchey, editor, Proceedings of FAABS II, volume 2699 of LNCS. Springer Verlag, 2003.
• [17] A. Lomuscio, R. Meyden, and M. Ryan. Knowledge in multi-agent systems: Initial configurations and broadcast. ACM Transactions of Computational Logic, 1(2), 2000.
• [18] A. Lomuscio, F. Raimondi, and M. Sergot. Towards model checking interpreted systems. In Proceedings of Mochart — First International Workshop on Model Checking and Artificial Intelligence, 2002.
• [19] A. Lomuscio and M. Sergot. Deontic interpreted systems. Studia Logica, 75, 2003.
• [20] M.-P. H. M. Wooldridge, M. Fisher and S. Parsons. Model checking multiagent systems with mable. In Proceedings of the First International Conference on Autonomous Agents and Multiagent Systems (AAMAS-02), Bologna, Italy, July 2002.
• [21] Z. Manna and A. Pnueli. The temporal logic of reactive and concurrent systems, volume 1. Springer-Verlag, Berlin/New York, 1992.
• [22] R. v. Meyden and K. Wong. Complete axiomatizations for reasoning about knowledge and branching time. Studia Logica, 75, 2003.
• [23] J.-J. C. Meyer and R. J. Wieringa. Deontic logic: A concise overview. In Deontic Logic in Computer Science, Wiley Professional Computing Series, chapter 1, pages 3-16. John Wiley and Sons, Chichester, UK, 1993.
• [24] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proc. of the 38th Design Automation Conference (DAC01), pages 530-535, June 2001.
• [25] W. Penczek and A. Lomuscio. Verifying epistemic properties of multi-agent systems via bounded model checking. In T. Sandholm, editor, Proceedings of the Second International Joint Conference on Autonomous Agents and Multi-agent systems (AAMAS-03), 2003.
• [26] W. Penczek, B. Wo´zna, and A. Zbrzezny. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 51(1-2):135-156, 2002.
• [27] A. S. Rao and M. P. Georgeff. Decision procedures for BDI logics. Journal of Logic and Computation, 8(3):293-343, June 1998.
• [28] M. Wooldridge. Computationally grounded theories of agency. In E. Durfee, editor, Proceedings of ICMAS, International Conference of Multi-Agent Systems. IEEE Press, 2000.