PSPACE bounds for rank-1 modal logics

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

PSPACE bounds for rank-1 modal logics

Full text

Pdf (280 KB)

Source

ACM Transactions on Computational Logic (TOCL) archive
Volume 10 , Issue 2 (February 2009) table of contents

Article No. 13

Year of Publication: 2009

ISSN:1529-3785

Authors

LUTZ Schröder	DFKI Bremen and Universität Bremen, Bremen, Germany
Dirk Pattinson	Imperial College London, London, UK

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 68, Citation Count: 0

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1462179.1462185 What is a DOI?

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

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Michael Barr, Terminal coalgebras in well-founded set theory, Theoretical Computer Science, v.114 n.2, p.299-315, June 21, 1993 [doi>10.1016/0304-3975(93)90076-6]
	2	Falk Bartels, Generalised coinduction, Mathematical Structures in Computer Science, v.13 n.2, p.321-348, April 2003 [doi>10.1017/S0960129502003900]
	3	Falk Bartels , Ana Sokolova , Erik de Vink, A hierarchy of probabilistic system types, Theoretical Computer Science, v.327 n.1-2, p.3-22, 25 October 2004 [doi>10.1016/j.tcs.2004.07.019]
	4	Patrick Blackburn , Maarten de Rijke , Yde Venema, Modal logic, Cambridge University Press, New York, NY, 2001
	5	Ronald V. Book , Timothy J. Long , Alan L. Selman, Quantitative relativizations of complexity classes, SIAM Journal on Computing, v.13 n.3, p.461-487, August 1984 [doi>10.1137/0213030]
	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	Ashok K. Chandra , Dexter C. Kozen , Larry J. Stockmeyer, Alternation, Journal of the ACM (JACM), v.28 n.1, p.114-133, Jan. 1981 [doi>10.1145/322234.322243]
	9	Chellas, B. 1980. Modal Logic. Cambridge University Press, Cambridge.
	10	Corina Crstea , Dirk Pattinson, Modular construction of complete coalgebraic logics, Theoretical Computer Science, v.388 n.1-3, p.83-108, December, 2007 [doi>10.1016/j.tcs.2007.06.002]
	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	E. A. Emerson , Joseph Y. Halpern, Decision procedures and expressiveness in the temporal logic of branching time, Journal of Computer and System Sciences, v.30 n.1, p.1-24, Feb. 1985 [doi>10.1016/0022-0000(85)90001-7]
	15	Patrice Enjalbert , Luis Farinas del Cerro, Modal resolution in clausal form, Theoretical Computer Science, v.65 n.1, p.1-33, 15 June 1989 [doi>10.1016/0304-3975(89)90137-0]
	16	Ronald Fagin , Joseph Y. Halpern, Reasoning about knowledge and probability, Journal of the ACM (JACM), v.41 n.2, p.340-367, March 1994 [doi>10.1145/174652.174658]
	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	Joseph Y. Halpern , Yoram Moses, A guide to completeness and complexity for modal logics of knowledge and belief, Artificial Intelligence, v.54 n.3, p.319-379, April 1992 [doi>10.1016/0004-3702(92)90049-4]
	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	Alexander Kurz, Specifying coalgebras with modal logic, Theoretical Computer Science, v.260 n.1-2, p.119-138, June 6, 2001 [doi>10.1016/S0304-3975(00)00125-0]
	25	Ladner, R. 1977. The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput. 6, 467--480.
	26	Kim G. Larsen , Arne Skou, Bisimulation through probabilistic testing, Information and Computation, v.94 n.1, p.1-28, Sept. 1991 [doi>10.1016/0890-5401(91)90030-6]
	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	Hans Jürgen Ohlbach , Jana Koehler, Modal logics, description logics and arithmetic reasoning, Artificial Intelligence, v.109 n.1-2, p.1-31, April 1999 [doi>10.1016/S0004-3702(99)00011-9]
	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	Dirk Pattinson, Semantical Principles in the Modal Logic of Coalgebras, Proceedings of the 18th Annual Symposium on Theoretical Aspects of Computer Science, p.514-526, February 15-17, 2001
	31	Dirk Pattinson, Coalgebraic modal logic: soundness, completeness and decidability of local consequence, Theoretical Computer Science, v.309 n.1, p.177-193, 2 December 2003 [doi>10.1016/S0304-3975(03)00201-9]
	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	Alexander Schrijver, Theory of linear and integer programming, John Wiley & Sons, Inc., New York, NY, 1986
	39	Schröder, L. 2007. A finite model construction for coalgebraic modal logic. J. Logic Algebraic Program. 73, 97--110.
	40	Lutz Schröder, Expressivity of coalgebraic modal logic: The limits and beyond, Theoretical Computer Science, v.390 n.2-3, p.230-247, January, 2008 [doi>10.1016/j.tcs.2007.09.023]
	41	Lutz Schroder , Dirk Pattinson, PSPACE Bounds for Rank-1 Modal Logics, Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, p.231-242, August 12-15, 2006 [doi>10.1109/LICS.2006.44]
	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	A. S. Troelstra , H. Schwichtenberg, Basic proof theory, Cambridge University Press, New York, NY, 1996
	45	Daniele Turi , Gordon Plotkin, Towards a Mathematical Operational Semantics, Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, p.280, June 29-July 02, 1997
	46	Wiebe van der Hoek , John-Jules Ch. Meyer, Graded Modalities in Epistemic Logic, Proceedings of the Second International Symposium on Logical Foundations of Computer Science, p.503-514, July 20-24, 1992
	47	M. Vardi, On the complexity of epistemic reasoning, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.243-252, June 1989, Pacific Grove, California, United States
	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	Yde Venema, Automata and fixed point logic: a coalgebraic perspective, Information and Computation, v.204 n.4, p.637-678, April 2006 [doi>10.1016/j.ic.2005.06.003]