The Complexity of Model Checking Concurrent Programs Against CTLK Specifications

  • Alessio Lomuscio
  • Franco Raimondi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4327)


This paper presents complexity results for model checking formulae of CTLK (a logic to reason about time and knowledge in multi-agent systems) in concurrent programs. We apply these results to evaluate the complexity of verifying programs of two model checkers for multi-agent systems: mcmas and Verics.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Benerecetti, M., Giunchiglia, F., Serafini, L.: Model checking multiagent systems. Journal of Logic and Computation 8(3), 401–423 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press, Cambridge (2001)zbMATHGoogle Scholar
  3. 3.
    Bordini, R.H., Fisher, M., Pardavila, C., Wooldridge, M.: Model checking AgentSpeak. In: Rosenschein, J.S., Sandholm, T., Michael, W., Yokoo, M. (eds.) Proceedings of the Second International Joint Conference on Autonomous Agents and Multi-agent systems (AAMAS 2003), pp. 409–416. ACM Press, New York (2003)CrossRefGoogle Scholar
  4. 4.
    Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)zbMATHCrossRefGoogle Scholar
  5. 5.
    Bryant, R.E.: On the complexity of VLSI implementations and graph representations of boolean functions with application to integer multiplication. IEEE Trans. Comput. 40(2), 205–213 (1991)CrossRefMathSciNetGoogle Scholar
  6. 6.
    Cheng, A.: Complexity results for model checking. Technical Report RS-95-18, BRICS - Basic Research in Computer Science, Department of Computer Science, University of Aarhus (February 1995)Google Scholar
  7. 7.
    Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV2: An open-source tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  8. 8.
    Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications: A practical approach. ACM Transactions on Programming Languages and Systems 8(2), 244–263 (1986)zbMATHCrossRefGoogle Scholar
  9. 9.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)Google Scholar
  10. 10.
    Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)zbMATHGoogle Scholar
  11. 11.
    Franceschet, M., Montanari, A., de Rijke, M.: Model checking for combined logics with an application to mobile systems. Automated Software Engineering 11, 289–321 (2004)CrossRefGoogle Scholar
  12. 12.
    Gabbay, D., Shehtman, V.: Products of modal logics, part 1. Logic Journal of the IGPL 6(1), 73–146 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Gammie, P., van der Meyden, R.: MCK: Model checking the logic of knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 479–483. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  14. 14.
    Greenlaw, R., Hoover, H.J., Ruzzo, W.L.: Limits to Parallel Computation: P-Completeness Theory. Oxford University Press, Oxford (1995)zbMATHGoogle Scholar
  15. 15.
    Hoek, W.v., Lomuscio, A., Wooldridge, M.: On the complexity of practical atl model checking knowledge, strategies, and games in multi-agent systems. In: Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems (AAMAS 2006), Hakodake, Japan. ACM Press, New York (to appear, 2006)Google Scholar
  16. 16.
    Holzmann, G.J.: The model checker SPIN. IEEE transaction on software engineering 23(5), 279–295 (1997)CrossRefMathSciNetGoogle Scholar
  17. 17.
    Huth, M.R.A., Ryan, M.D.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, Cambridge (2000)zbMATHGoogle Scholar
  18. 18.
    Kacprzak, M., Lomuscio, A., Penczek, W.: From bounded to unbounded model checking for temporal epistemic logic. Fundamenta Informaticae 63(2,3), 221–240 (2004)zbMATHMathSciNetGoogle Scholar
  19. 19.
    Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. Journal of the ACM 47(2), 312–360 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Lomuscio, A., Łasica, T., Penczek, W.: Bounded model checking for interpreted systems: preliminary experimental results. In: Hinchey, M.G., Rash, J.L., Truszkowski, W.F., Rouff, C.A., Gordon-Spears, D.F. (eds.) FAABS 2002. LNCS, vol. 2699, pp. 115–125. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  21. 21.
    Lomuscio, A., Raimondi, F.: The complexity of model checking concurrent programs against CTLK specifications. In: Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems (AAMAS 2006), Hakodake, Japan, pp. 548–550. ACM Press, New York (2006)CrossRefGoogle Scholar
  22. 22.
    Lomuscio, A., Raimondi, F.: MCMAS: A model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 450–454. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  23. 23.
    McMillan, K.: The SMV system. Technical Report CMU-CS-92-131. Carnegie-Mellon University (Febuary 1992)Google Scholar
  24. 24.
    McMillan, K.: Symbolic model checking: An approach to the state explosion problem. Kluwer Academic Publishers, Dordrecht (1993)Google Scholar
  25. 25.
    McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)zbMATHGoogle Scholar
  26. 26.
    Meyden, R.: Common knowledge and update in finite environments. Information and Computation 140(2), 115–157 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  27. 27.
    van der Meyden, R., Shilov, N.V.: Model checking knowledge and time in systems with perfect recall. In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 432–445. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  28. 28.
    Nabialek, W., Niewiadomski, A., Penczek, W., Pólrola, A., Szreter, M.: VerICS 2004: A model checker for real time and multi-agent systems. In: Proceedings of the International Workshop on Concurrency, Specification and Programming (CS&P 2004). Informatik-Berichte, vol. 170, pp. 88–99. Humboldt University (2004)Google Scholar
  29. 29.
    Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)zbMATHGoogle Scholar
  30. 30.
    Raimondi, F., Lomuscio, A.: Automatic verification of multi-agent systems by model checking via OBDDs. Journal of Applied Logic (2005); Special issue on Logic-based agent verification (to appear)Google Scholar
  31. 31.
    Schnoebelen, P.: The complexity of temporal logic model checking. In: Proceedings of the 4th Conference Advances in Modal Logic (AiML 2002). Advances in Modal Logic, vol. 4, pp. 437–459. King’s College Publications (2003)Google Scholar
  32. 32.
    Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. Journal of the ACM 32(3), 733–749 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  33. 33.
    Wooldridge, M.: Reasoning about Rational Agents. MIT Press, Cambridge (2000)zbMATHGoogle Scholar
  34. 34.
    Wooldridge, M.: An introduction to multi-agent systems. John Wiley, England (2002)Google Scholar
  35. 35.
    Wooldridge, M., Fisher, M., Huget, M., Parsons, S.: Model checking multiagent systems with MABLE. In: Proceedings of the First International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2002), Bologna, Italy, pp. 952–959 (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Alessio Lomuscio
    • 1
  • Franco Raimondi
    • 1
  1. 1.Department of Computer ScienceUniversity College LondonLondonUK

Personalised recommendations