Abstract
This paper deals with the problem of verification of game-like structures by means of symbolic model checking. Alternating-time Temporal Epistemic Logic (ATEL) is used for expressing properties of multi-agent systems represented by alternating epistemic temporal systems as well as concurrent epistemic game structures. Unbounded model checking (a SAT based technique) is applied for the first time to verification of ATEL. An example is given to show an application of the technique.
This work relates to Department of the Navy Grant N000I4-04-1-4080 issued by the Office of Naval Research International Field Office. The United States Government has a royalty-free license throughout the world in all copyrightable material contained herein. The first author acknowledges also support from the Polish National Committee for Scientific Research under Bialystok University of Technology (grant W/IMF/2/04).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., L. de Alfaro, T. Henzinger, S. Krishnan, F. Mang, S. Qadeer, S. Rajamani, and S. Tasiran: 2000, MOCHA user manual. Technical report, University of California at Berkeley. http://www-cad.eecs.berkeley.edu/∼ mocha/doc/c-doc/cmanual.ps.gz.
Alur, R., T. A. Henzinger, and O. Kupferman: 1997, Alternating-time temporal logic, In Proceedings of the 38th IEEE Symposium on Foundations of Computer Science. (FOCS’97), IEEE Computer Society, pp. 100–109.
Alur, R., T. A. Henzinger, and O. Kupferman: 1998, Alternating-time temporal logic, LNCS 1536, 23–60.
Alur, R., T. A. Henzinger, and O. Kupferman: 2002, Alternating-time temporal logic, Journal of the ACM 49(5), 672–713.
Biere, A., A. Cimatti, E. Clarke, and Y. Zhu: 1999, Symbolic model checking without BDDs, In Proceedings of the Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99), Vol. 1579 of LNCS, Springer-Verlag, pp. 193–207.
Clarke, E., A. Biere, R. Raimi, and Y. Zhu: 2001, Bounded model checking using satisfiability solving, Formal Methods in System Design 19(l), 7–34.
Clarke, E. M., O. Grumberg, and D. Peled: 1999, Model Checking, MIT Press.
Davis, M., G. Logemann, and D. Loveland: 1962, A machine program for theorem proving, Journal of the ACM 5(7), 394–397.
Fagin, R., J. Y. Halpern, Y. Moses, and M. Y. Vardi: 1995, Reasoning about Knowledge, MIT Press, Cambridge.
Goranko, V. and W. Jamroga: 2004, Comparing semantics for logics of multi-agent systems. Synthese 139(2), 241–280. Available from http://journals.kluweronline.com/article.asp? PIPS=5264999.
Jamroga, W. and W. van der Hoek: 2004, Agents that know how to play, Fundamenta Informaticae. To appear.
Jamroga, W., W. van der Hoek, and M. Wooldridge: 2004, Obligations vs. abilities of agents via deontic ATL. Accepted for the Seventh International Workshop on Deontic Logic in Computer Science DEON’04. To appear in LNCS.
Kacprzak, M., A. Lomuscio, T. Lasica, W. Penczek, and M. Szreter: 2004a, Verifying multiagent systems via unbounded model checking, In Proceedings of the Third NASA Workshop on Formal Approaches to Agent-Based Systems (FAABS III), LNCS, Springer-Verlag. To appear.
Kacprzak, M., A. Lomuscio, and W. Penczek: 2004b, Verification of multi-agent systems via unbounded model checking In N. R. Jennings, C. Sierra, L. Sonenberg, and M. Tambe (eds.), Proceedings of the Third International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS’04), Vol.II, ACM pp. 638–645.
Kacprzak, M., A. Lomuscio, and W. Penczek: 2003, Unbounded model checking for knowledge and time. Technical Report 966, ICS PAS, Ordona 21, 01-237 Warsaw. Also available at http://www.ipipan.waw.pl/~penczek/WPenczek/2003.html.
Kacprzak, M., and W. Penczek: 2004, Unbounded model checking for alternating-time temporal logic, In N. R. Jennings, C. Sierra, L. Sonenberg, and M. Tambe (eds.), Proceedings of the Third International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS’04), Vol.II, ACM pp.646–653.
Lomuscio, A., T. Lasica, and W. Penczek: 2003, Bounded model checking for interpreted systems: Preliminary experimental results, In Proceedings of the second NASA Workshop on Formal Approaches to Agent-Based Systems (FAABS’02), Vol.2699 of LNAI, Springer-Verlag, pp.115–125.
McMillan, K. L.: 1993, Symbolic Model Checking. Kluwer Academic Publishers.
McMillan, K. L.: 2002, Applying SAT methods in unbounded symbolic model checking, In Proceedings of the 14th International Conference on Computer Aided Verification (CAV’02), Vol.2404 of LNCS, Springer-Verlag, pp.250–264.
Penczek, W. and A. Lomuscio: 2003a, Verifying epistemic properties of multi-agent systems via bounded model checking, Fundamenta Informaticae 55(2), 167–185.
Penczek, W. and A. Lomuscio: 2003b, Verifying epistemic properties of multi-agent systems via bounded model checking, In T. Sandholm (ed.), Proceedings of the second International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS’03), ACM, pp.209–216.
Raimondi, F. and A. Lomuscio: 2003, A tool for specification and verification of epistemic and temporal properties of multi-agent system, Electronic Lecture Notes in Theoretical Computer Science. To appear.
Robinson S.: 2004, How real people think in strategic games, SIAM News, 37(1).
Tarski, A.: 1995, A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics 5: 285–309.
van der Hoek W. and M. Wooldridge: 2002a, Model checking knowledge and time, In Proceedings of the Ninth International SPIN Workshop (SPIN’02), Vol.2318 of LNCS, Springer-Verlag, pp.95–111.
van der Hoek W. and M. Wooldridge: 2002b, Tractable multiagent planning for epistemic goals, In Proceedings of the First International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS’02), Vol. III, ACM, pp.1167–1174.
van der Hoek W. and M. Wooldridge: 2003, Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications, Studia Logica 75(1), 125–157.
van der Meyden R. and H. Shilov: 1999, Model checking knowledge and time in systems with perfect recall, In Proceedings of the 19th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’99), Vol.1738 of LNCS, Springer-Verlag, pp. 432–445.
van Otterloo, S., W. van der Hoek, and M. Wooldridge: 2003, Knowledge as strategic ability, ENCTS, 85(2), 1–23.
Wooldridge, M.: 2002, An introduction to multi-agent systems, John Wiley, England.
Wooldridge, M., M. Fisher, M. P. Huget, and S. Parsons: 2002, Model checking multiagent systems with MABLE, In Proceedings of the 1st International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS’02), Vol.II, ACM, pp. 952–959.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2004 Kluwer Academic Publishers
About this chapter
Cite this chapter
Kacprzak, M., Penczek, W. (2004). A Sat-Based Approach to Unbounded Model Checking for Alternating-Time Temporal Epistemic Logic. In: Information, Interaction and Agency. Springer, Dordrecht. https://doi.org/10.1007/1-4020-4094-6_9
Download citation
DOI: https://doi.org/10.1007/1-4020-4094-6_9
Publisher Name: Springer, Dordrecht
Print ISBN: 978-1-4020-3600-2
Online ISBN: 978-1-4020-4094-8
eBook Packages: Humanities, Social Sciences and LawPhilosophy and Religion (R0)