The Completeness Problem for Modal Logic

  • Antonis AchilleosEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10703)


We introduce the completeness problem for Modal Logic and examine its complexity. For a definition of completeness for formulas, given a formula of a modal logic, the completeness problem asks whether the formula is complete for that logic. We discover that completeness and validity have the same complexity — with certain exceptions for which there are, in general, no complete formulas. To prove upper bounds, we present a non-deterministic polynomial-time procedure with an oracle from PSPACE that combines tableaux and a test for bisimulation, and determines whether a formula is complete.


Modal logic Completeness Computational complexity Bisimulation 



The author is grateful to Luca Aceto for valuable comments that helped improve the quality of this paper.


  1. 1.
    Ladner, R.E.: The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput. 6(3), 467–480 (1977)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Halpern, J.Y., Rêgo, L.C.: Characterizing the NP-PSPACE gap in the satisfiability problem for modal logic. J. Logic Comput. 17(4), 795–806 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Halpern, J.Y., Moses, Y.: A guide to completeness and complexity for modal logics of knowledge and belief. Artif. Intell. 54(3), 319–379 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Artemov, S.: Syntactic epistemic logic. In: Book of Abstracts, 15th Congress of Logic, Methodology and Philosophy of Science CLMPS 2015, pp. 109–110 (2015)Google Scholar
  5. 5.
    Artemov, S.: Syntactic epistemic logic and games (2016)Google Scholar
  6. 6.
    Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM (JACM) 32(1), 137–161 (1985)CrossRefzbMATHGoogle Scholar
  7. 7.
    Milner, R.: Communication and Concurrency. Prentice-Hall Inc., Upper Saddle River (1989)zbMATHGoogle Scholar
  8. 8.
    Graf, S., Sifakis, J.: A modal characterization of observational congruence on finite terms of CCS. Inf. Control 68(1–3), 125–145 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Steffen, B., Ingólfsdóttir, A.: Characteristic formulas for processes with divergence. Inf. Comput. 110(1), 149–163 (1994)CrossRefzbMATHGoogle Scholar
  10. 10.
    Mller-Olm, M.: Derivation of characteristic formulae. Electr. Notes Theor. Comput. Sci. 18, 159–170 (1998)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Aceto, L., Della Monica, D., Fábregas, I., Ingólfsdóttir, A.: When are prime formulae characteristic? In: Italiano, G.F., Pighizzini, G., Sannella, D.T. (eds.) MFCS 2015. LNCS, vol. 9234, pp. 76–88. Springer, Heidelberg (2015). CrossRefGoogle Scholar
  12. 12.
    Fine, K.: Normal forms in modal logic. Notre Dame J. Formal Logic 16(2), 229–237 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Achilleos, A.: The completeness problem for modal logic. CoRR abs/1605.01004 (2016)Google Scholar
  14. 14.
    Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2001)CrossRefzbMATHGoogle Scholar
  15. 15.
    Chagrov, A., Zakharyaschev, M.: Modal Logic. Oxford University Press, Oxford (1997)zbMATHGoogle Scholar
  16. 16.
    Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Fitting, M.: Tableau methods of proof for modal logics. Notre Dame J. Formal Logic 13(2), 237–247 (1972)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Massacci, F.: Single step tableaux for modal logics. J. Autom. Reasoning 24(3), 319–364 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    D’Agostino, M., Gabbay, D.M., Hähnle, R., Posegga, J.: Handbook of Tableau Methods. Springer, Dordrecht (1999). CrossRefzbMATHGoogle Scholar
  20. 20.
    Blass, A., Gurevich, Y.: On the unique satisfiability problem. Inf. Control 55(1–3), 80–88 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Moss, L.S.: Finite models constructed from canonical formulas. J. Philos. Logic 36(6), 605–640 (2007)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2018

Authors and Affiliations

  1. 1.School of Computer ScienceReykjavik UniversityReykjavikIceland

Personalised recommendations