Abstract
We revise the model checking algorithm for combination of Computation Tree Logic and Propositional Logic of Knowledge in finite multiagent systems with a perfect recall synchronous semantics. A new approach is based on data structures that are exponentially smaller than the structures used in the previous versions of the model checking algorithm. It reduces the time complexity of the algorithm exponentially.
The research has been supported by Russian Foundation for Basic Research (grant 10-01-00532-a) and by Siberian Branch of Russian Academy of Science (Integration Grant n.2/12).
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
Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation 160(1-2), 109–127 (2000)
Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Verifying Multi-agent Programs by Model Checking. Autonomous Agents and Multi-Agent Systems 12(2), 239–256 (2006)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic Model Checking: 1020 states and beyond. Information and Computation 98(2), 142–170 (1992)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)
Cohen, M., Lomuscio, A.: Non-elementary speed up for model checking synchronous perfect recall. In: Proceeding of the 2010 Conference on ECAI 2010, pp. 1077–1078. IOS Press, Amsterdam (2010)
Emerson, E.A.: Temporal and Modal Logic. In: Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. Elsevier and MIT Press (1990)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press (1995)
Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comp. Sci. 256(1-2), 63–92 (2001)
Garanina, N.O., Kalinina, N.A., Shilov, N.V.: Model checking knowledge, actions and fixpoints. In: Proc. of Concurrency, Specification and Programming Workshop CS&P 2004, Germany. Humboldt Universitat, Berlin (2004); Informatik-Bericht Nr. 170(2), 351–357
Halpern, J.Y., van der Meyden, R., Vardi, M.Y.: Complete Axiomatizations for Reasoning About Knowledge and Time. SIAM J. Comp. 33(3), 674–703 (2004)
Huang, X., van der Meyden, R.: The Complexity of Epistemic Model Checking: Clock Semantics and Branching Time. In: Proc. of 19th ECAI, Lisbon, Portugal, August 16-20. Frontiers in Artificial Intelligence and Applications, vol. 215, pp. 549–554. IOS Press (2010)
Kozen, D.: Results on the Propositional Mu-Calculus. Theoretical Computer Science 27(3), 333–354 (1983)
Kozen, D., Tiuryn, J.: Logics of Programs. In: Handbook of Theoretical Computer Science, vol. B, pp. 789–840. Elsevier and MIT Press (1990)
Kwiatkowska, M.Z., Lomuscio, A., Qu, H.: Parallel Model Checking for Temporal Epistemic Logic. In: Proc. of 19th ECAI, Lisbon, Portugal, August 16-20. Frontiers in Artificial Intelligence and Applications, vol. 215, pp. 543–548. IOS Press (2010)
Lomuscio, A., Penczek, W., Qu, H.: Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems. In: Proc. of 9th AAMAS, Toronto, Canada, May 10-14. IFAAMAS, vol. 1, pp. 659–666 (2010)
van der Meyden, R., Shilov, N.V.: Model Checking Knowledge and Time in Systems with Perfect Recall. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 432–445. Springer, Heidelberg (1999)
Rescher, N.: Epistemic Logic. A Survey of the Logic of Knowledge. University of Pitsburgh Press (2005)
Shilov, N.V., Yi, K.: How to find a coin: propositional program logics made easy. In: Current Trends in Theoretical Computer Science, vol. 2, pp. 181–213. World Scientific (2004)
Shilov, N.V., Garanina, N.O., Choe, K.-M.: Update and Abstraction in Model Checking of Knowledge and Branching Time. Fundameta Informaticae 72(1-3), 347–361 (2006)
Shilov, N.V., Garanina, N.O.: Well-Structured Model Checking of Multiagent Systems. In: Virbitskaite, I., Voronkov, A. (eds.) PSI 2006. LNCS, vol. 4378, pp. 363–376. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Garanina, N.O. (2012). Exponential Acceleration of Model Checking for Perfect Recall Systems. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds) Perspectives of Systems Informatics. PSI 2011. Lecture Notes in Computer Science, vol 7162. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29709-0_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-29709-0_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29708-3
Online ISBN: 978-3-642-29709-0
eBook Packages: Computer ScienceComputer Science (R0)