PSPACE bounds for rank-1 modal logics

Abstract

For lack of general algorithmic methods that apply to wide classes of logics, establishing a complexity bound for a given modal logic is often a laborious task. The present work is a step towards a general theory of the complexity of modal logics. Our main result is that all rank-1 logics enjoy a shallow model property and thus are, under mild assumptions on the format of their axiomatisation, in PSPACE. This leads to a unified derivation of tight PSPACE-bounds for a number of logics, including K, KD, coalition logic, graded modal logic, majority logic, and probabilistic modal logic. Our generic algorithm moreover finds tableau proofs that witness pleasant proof-theoretic properties including a weak subformula property. This generality is made possible by a coalgebraic semantics, which conveniently abstracts from the details of a given model class and thus allows covering a broad range of logics in a uniform way.

References

1. Barr, M. 1993. Terminal coalgebras in well-founded set theory. Theor. Comput. Sci. 114, 299--315.
2. Bartels, F. 2003. Generalised coinduction. Math. Struct. Comput. Sci. 13, 321--348.
3. Bartels, F., Sokolova, A., and de Vink, E. P. 2004. A hierarchy of probabilistic system types. Theor. Comput. Sci. 327, 3--22.
4. Blackburn, P., de Rijke, M., and Venema, Y. 2001. Modal Logic. Cambridge University Press, Cambridge.
5. Book, R., Long, T., and Selman, A. 1984. Quantitative relativizations of complexity classes. SIAM J. Comput. 13, 461--487.
6. Carlyle, J. W. and Paz, A. 1971. Realizations by stochastic finite automata. J. Comput. Syst. Sci. 5, 26--40.
7. Caro, F. D. 1988. Graded modalities II (canonical models). Studia Logica 47, 1--10.
8. Chandra, A., Kozen, D., and Stockmeyer, L. 1981. Alternation. J. ACM 28, 114--133.
9. Chellas, B. 1980. Modal Logic. Cambridge University Press, Cambridge.
10. Cîrstea, C. and Pattinson, D. 2007. Modular construction of complete coalgebraic logics. Theor. Comput. Sci. 388, 83--108.
11. D'Agostino, G. and Visser, A. 2002. Finality regained: A coalgebraic study of Scott-sets and multisets. Arch. Math. Logic 41, 267--298.
12. De Nivelle, H., Schmidt, R. A., and Hustadt, U. 2000. Resolution-Based methods for modal logics. Logic J. IGPL 8, 265--292.
13. Demri, S. and Lugiez, D. 2006. Presburger modal logic is only PSPACE-complete. In Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR'06), U. Furbach and N. Shankar, Eds. Lecture Notes in Artificial Intelligence, vol. 4130. Springer, Berlin, 541--556. Full version available as Res. rep. LSV-06-15, Laboratoire Spécification et Vérification, Ecole Normale Supérieure de Cachan.
14. Emerson, E. A. and Halpern, J. Y. 1985. Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Syst. Sci. 30, 1--24.
15. Enjalbert, P. and del Cerro, L. F. 1989. Modal resolution in clausal form. Theor. Comput. Sci. 65, 1--33.
16. Fagin, R. and Halpern, J. Y. 1994. Reasoning about knowledge and probability. J. ACM 41, 340--367.
17. Fine, K. 1972. In so many possible worlds. Notre Dame J. Formal Logic 13, 516--520.
18. Halpern, J. and Rêgo, L. C. 2007. Characterizing the NP-PSPACE gap in the satisfiability problem for modal logic. In Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI'07), M. M. Veloso, Ed. 2306--2311.
19. Halpern, J. Y. and Moses, Y. O. 1992. A guide to completeness and complexity for modal logics of knowledge and belief. Artif. Intell. 54, 319--379.
20. Hansen, H. H. and Kupke, C. 2004. A coalgebraic perspective on monotone modal logic. In Coalgebraic Methods in Computer Science, J. Adámek and S. Milius, Eds. Electronic Notes in Theoretical Computer Science, vol. 106. Elsevier, Amsterdam, 121--143.
21. Heifetz, A. and Mongin, P. 2001. Probabilistic logic for type spaces. Games Econom. Behav. 35, 31--53.
22. Jacobs, B. 2000. Towards a duality result in coalgebraic modal logic. Coalgebraic Methods in Computer Science Workshop, H. Reichel, Ed. Electronic Notes in Theoretical Computer Science, vol. 33. Elsevier, Amsterdam.
23. Kupke, C., Kurz, A., and Pattinson, D. 2005. Ultrafilter extensions for coalgebras. In Proceedings of the 1st International Conference on Algebra and Coalgebra in Computer Science (CALCO'05), J. L. Fiadeiro et al. Eds. Lecture Notes in Computer Science, vol. 3629. Springer, Berlin, 263--277.
24. Kurz, A. 2001. Specifying coalgebras with modal logic. Theor. Comput. Sci. 260, 119--138.
25. Ladner, R. 1977. The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput. 6, 467--480.
26. Larsen, K. and Skou, A. 1991. Bisimulation through probabilistic testing. Inf. Comput. 94, 1--28.
27. Mossakowski, T., Schröder, L., Roggenbach, M., and Reichel, H. 2006. Algebraic-coalgebraic specification in CoCASL. J. Logic Algebraic Program. 67, 146--197.
28. Ohlbach, H. J. and Koehler, J. 1999. Modal logics, description logics and arithmetic reasoning. Artig. Intel. 109, 1--31.
29. Pacuit, E. and Salame, S. 2004. Majority logic. In Proceedings of the 9th International Conference on Principles of Knowledge Representation and Reasoning (KR'04), D. Dubois et al. Eds. AAAI Press, 598--605.
30. Pattinson, D. 2001. Semantical principles in the modal logic of coalgebras. In Proceedings of the 18th Annual Symposium on Theoretical Aspects of Computer Science (STACS'01). A. Ferreira and H. Reichel, Eds. Lecture Notes in Computer Science, vol. 2010. Springer, Berlin, 514--526.
31. Pattinson, D. 2003. Coalgebraic modal logic: Soundness, completeness and decidability of local consequence. Theor. Comput. Sci. 309, 177--193.
32. Pattinson, D. 2004. Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Logic 45, 19--33.
33. Pauly, M. 2002. A modal logic for coalitional power in games. J. Logic Comput. 12, 149--166.
34. Pauly, M. 2005. On the role of language in social choice theory. Unpublished manuscript.
35. Rabin, M. 1963. Probabilistic automata. Inf. Control 6, 230--245.
36. Rößiger, M. 2000. Coalgebras and modal logic. In Coalgebraic Methods in Computer Science (CMCS'00), H. Reichel, Ed. Electronic Notes in Theoretical Computer Science, vol. 33. Elsevier, Amsterdam.
37. Rothe, J., Tews, H., and Jacobs, B. 2001. The Coalgebraic Class Specification Language CCSL. J. Universal Comput. Sci. 7, 175--193.
38. Schrijver, A. 1986. Theory of Linear and Integer Programming. John Wiley & Sons, Chichester, UK.
39. Schröder, L. 2007. A finite model construction for coalgebraic modal logic. J. Logic Algebraic Program. 73, 97--110.
40. Schröder, L. 2007. Expressivity of coalgebraic modal logic: The limits and beyond. Theor. Comput. Sci. 390, 230--247.
41. Schröder, L. and Pattinson, D. 2006. PSPACE reasoning for rank-1 modal logics. In Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science (LICS'06), R. Alur, Ed. IEEE Computer Society Press, 231--240. Presentation slides available under www.informatik.uni-bremen.de/~lschrode/slides/rank1pspace.pdf.
42. Schröder, L. and Pattinson, D. 2007. Modular algorithms for heterogeneous modal logics. In Proceedings of the 34th International Colloquium on Automata, Languages and Programming (ICALP'07) L. Avge et al., Eds. Lecture Notes in Computer Science, vol. 4596. Springer, Berlin, 459--471.
43. Tobies, S. 2001. PSPACE reasoning for graded modal logics. J. Logic Comput. 11, 85--106.
44. Troelstra, A. S. and Schwichtenberg, H. 1996. Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science, vol. 43. Cambridge University Press, Cambridge.
45. Turi, D. and Plotkin, G. 1997. Towards a mathematical operational semantics. In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97). IEEE Computer Society Press, 280--291.
46. van der Hoek, W. and Meyer, J.-J. 1992. Graded modalities in epistemic logic. In Proceedings of the 2nd International Symposium on Logical Foundations of Computer Science (LFCS'92), A. Nerode and M. A. Taitslin, Eds. Lecture Notes in Computer Science, vol. 620. Springer, Berlin, 503--514.
47. Vardi, M. 1989. On the complexity of epistemic reasoning. In Proceedings of the 4th Annual IEEE Symposium on Logic in Computer Science (LICS'89). IEEE Computer Society Press, 243--251.
48. Vardi, M. Y. 1996. Why is modal logic so robustly decidable? In Proceedings of the DIMACS Workshop on Descriptive Complexity and Finite Models, N. Immerman and P. G. Kolaitis, Eds. DIMACS Series. Discrete Mathematics and Theoretical Computer Science, vol. 31. American Mathematical Society, 149--184.
49. Venema, Y. 2006. Automata and fixed point logics: A coalgebraic perspective. Inf. Comput. 204, 637--678.

Index Terms

• Theory of computation

  • Computational complexity and cryptography

    • Interactive proof systems

    • Proof complexity

  • Logic

    • Modal and temporal logics

    • Proof theory