From Bounded to Unbounded Model Checking for Temporal Epistemic Logic

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

Abstrakty

EN

This paper addresses the problem of verification of temporal epistemic properties of multi-agent systems by means of symbolic model checking. An overview of the technique of bounded model checking for temporal epistemic logic, and an analysis of some limitations of the method are provided. An extension of this technique called unbounded model checking to solve these limitations is explored. Similarities and differences of the two methods are explicitly exemplified by the analysis of a scenario in the two formalisms.

Słowa kluczowe

EN

multi-agent systems; temporal epistemic logic; model checking

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 63, nr 2,3
• Strony: 221--240
• Opis fizyczny: Bibliogr. 19 poz., rys.

Twórcy

autor

Kacprzak M.

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

autor

Lomuscio A.

• Department of Computer Science, King’s College London, London WC2R 2LS, United Kingdom

autor

Penczek W.

• Institute of Computer Science, PAS, 01-237 Warsaw, ul. Ordona 21, Poland

Bibliografia

• [1] A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. of the 5th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99), volume 1579 of LNCS, pages 193-207. Springer-Verlag, 1999.
• [2] R. H. Bordini, M. Fisher, C. Pardavila, and M. Wooldridge. Model checking agent speak. In J. S. Rosenschein, T. Sandholm, W. Michael, and M. Yokoo, editors, Proceedings of the Second International Joint Conference on Autonomous Agents and Multi-agent systems (AAMAS-03), pages 409-416. ACM Press, 2003.
• [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. A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999.
• [5] M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Journal of the ACM, 5(7):394-397, 1962.
• [6] E. A. Emerson and E. M. Clarke. Characterizing correctness properties of parallel programs using fixpoints. In Proc. of the 7th Int. Colloquium on Automata, Languages and Programming (ICALP’80), volume 85 of LNCS, pages 169-181. Springer-Verlag, 1980.
• [7] 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.
• [8] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, 1995.
• [9] A. Lomuscio, T. Łasica, and W. Penczek. Bounded model checking for interpreted systems: Preliminary experimental results. In Proc. of the 2nd NASA Workshop on Formal Approaches to Agent-Based Systems (FAABS’02), volume 2699 of LNAI, pages 115-125. Springer-Verlag, 2003.
• [10] Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1992.
• [11] K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
• [12] K. L. McMillan. Applying SAT methods in unbounded symbolic model checking. In Proc. of the 14th Int. Conf. on Computer Aided Verification (CAV’02), volume 2404 of LNCS, pages 250-264. Springer-Verlag, 2002.
• [13] W. Penczek and A. Lomuscio. Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae, 55(2):167-185, 2003.
• [14] W. Penczek, B. Woźna, and A. Zbrzezny. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 51(1-2):135-156, 2002.
• [15] A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285-309, 1955.
• [16] 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.
• [17] 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), volume III, pages 1167-1174. ACM, July 2002.
• [18] R. van der Meyden and H. Shilov. Model checking knowledge and time in systems with perfect recall. In Proc. of the 19th Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’99), volume 1738 of LNCS, pages 432-445. Springer-Verlag, 1999.
• [19] M. Wooldridge. An introduction to multi-agent systems. JohnWiley, England, 2002