Abstract
We study the model checking problem for logics whose semantics are defined using transitive Kripke models. We show that the model checking problem is P-complete for the intuitionistic logic KC. Interestingly, for its modal companion S4.2 we also obtain P-completeness even if we consider formulas with one variable only. This result is optimal since model checking for S4 without variables is NC1-complete. The strongest variable free modal logic with P-complete model checking problem is K4. On the other hand, for KC formulas with one variable only we obtain much lower complexity, namely LOGDCFL as an upper bound.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
van Dalen, D.: Logic and Structure, 4th edn. Springer, Heidelberg (2004)
Chagrov, A., Zakharyaschev, M.: Modal Logic. Clarendon Press, Oxford (1997)
Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979)
Lynch, N.A.: Log space recognition and translation of parenthesis languages. J. ACM 24(4), 583–590 (1977)
Buss, S.R.: The Boolean formula value problem is in ALOGTIME. In: Proc. 19th STOC, pp. 123–131. ACM Press, New York (1987)
Dummett, M., Lemmon, E.: Modal logics between S4 and S5. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 14(24), 250–264 (1959)
Visser, A.: A propositional logic with explicit fixed points. Studia Logica 40, 155–175 (1980)
Ladner, R.: The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing 6(3), 467–480 (1977)
Spaan, E.: Complexity of Modal Logics. PhD thesis, Department of Mathematics and Computer Science. University of Amsterdam (1993)
Mundhenk, M., Weiß, F.: The model checking problem for intuitionistic logic with one variable is AC1 -complete (2010) (unpublished manuscript)
Chandra, A.K., Kozen, D., Stockmeyer, L.J.: Alternation. Journal of the Association for Computing Machinery 28, 114–133 (1981)
Greenlaw, R., Hoover, H.J., Ruzzo, W.L.: Limits to Parallel Computation: P-Completeness Theory. Oxford University Press, New York (1995)
Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)
Nishimura, I.: On formulas of one variable in intuitionistic propositional calculus. J. of Symbolic Logic 25, 327–331 (1960)
Makinson, D.: There are infinitely many Diodorean modal functions. J. of Symbolic Logic 31(3), 406–408 (1966)
Gabbay, D.M.: Semantical investigations in Heyting’s intuitionistic logic. D.Reidel, Dordrecht (1981)
Rybakov, M.N.: Complexity of intuitionistic and Visser’s basic and formal logics in finitely many variables. In: Papers from the 6th conference on “Advances in Modal Logic”, pp. 393–411. College Publications (2006)
O’Connor, M.: Embeddings into free Heyting algebras and translations into intuitionistic propositional logic. In: Artemov, S., Nerode, A. (eds.) LFCS 2007. LNCS, vol. 4514, pp. 437–448. Springer, Heidelberg (2007)
Fernandez, D.: A polynomial translation of S4 into intuitionistic logic. J. of Symbolic Logic 71(3), 989–1001 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mundhenk, M., Weiß, F. (2010). The Complexity of Model Checking for Intuitionistic Logics and Their Modal Companions. In: Kučera, A., Potapov, I. (eds) Reachability Problems. RP 2010. Lecture Notes in Computer Science, vol 6227. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15349-5_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-15349-5_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15348-8
Online ISBN: 978-3-642-15349-5
eBook Packages: Computer ScienceComputer Science (R0)