Exponential Acceleration of Model Checking for Perfect Recall Systems

  • Natalia O. Garanina
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7162)


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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    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)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    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)CrossRefGoogle Scholar
  3. 3.
    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)MathSciNetzbMATHCrossRefGoogle Scholar
  4. 4.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)Google Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    Emerson, E.A.: Temporal and Modal Logic. In: Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. Elsevier and MIT Press (1990)Google Scholar
  7. 7.
    Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press (1995)Google Scholar
  8. 8.
    Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comp. Sci. 256(1-2), 63–92 (2001)MathSciNetzbMATHCrossRefGoogle Scholar
  9. 9.
    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–357Google Scholar
  10. 10.
    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)zbMATHCrossRefGoogle Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    Kozen, D.: Results on the Propositional Mu-Calculus. Theoretical Computer Science 27(3), 333–354 (1983)MathSciNetzbMATHCrossRefGoogle Scholar
  13. 13.
    Kozen, D., Tiuryn, J.: Logics of Programs. In: Handbook of Theoretical Computer Science, vol. B, pp. 789–840. Elsevier and MIT Press (1990)Google Scholar
  14. 14.
    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)Google Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    Rescher, N.: Epistemic Logic. A Survey of the Logic of Knowledge. University of Pitsburgh Press (2005)Google Scholar
  18. 18.
    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)Google Scholar
  19. 19.
    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)MathSciNetzbMATHGoogle Scholar
  20. 20.
    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)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Natalia O. Garanina
    • 1
  1. 1.A.P. Ershov Institute of Informatics SystemsRussian Academy of ScienceNovosibirskRussia

Personalised recommendations