×

zbMATH — the first resource for mathematics

All finitely axiomatizable tense logics of linear time flows are coNP-complete. (English) Zbl 1096.03014
Summary: We prove that all finitely axiomatizable tense logics with temporal operators for ‘always in the future’ and ‘always in the past’ and determined by linear time flows are coNP-complete. It follows, for example, that all tense logics containing a density axiom of the form \(\square ^{n+1}_{F} p \rightarrow \square^{n}_{F} p\), for some \(n \geq 0\), are coNP-complete. Additionally, we prove coNP-completeness of all \(\cap\)-irreducible tense logics. As these classes of tense logics contain many Kripke incomplete bimodal logics, we obtain many natural examples of Kripke incomplete normal bimodal logics which are nevertheless coNP-complete.

MSC:
03B44 Temporal logic
03D15 Complexity of computation (including implicit computational complexity)
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
03B45 Modal logic (including the logic of norms)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Bezhanishvili, N., and I. Hodkinson, ’All normal extensions of S5-squared are finitely axiomatizable’, Studia Logica, 78:443–457, 2004. · Zbl 1069.03010 · doi:10.1007/s11225-004-6044-z
[2] Bezhanishvili, N., and M. Marx, ’All proper normal extensions of S5-square have the polynomial size model property’, Studia Logica, 73:367–382, 2003. · Zbl 1027.03015 · doi:10.1023/A:1023383112908
[3] Etessami, K., M. Vardi, and T.Wilke, ’First-order logic with two variables and unary temporal logic’, Information and Computation, 179:279–295, 2002. · Zbl 1096.03013 · doi:10.1006/inco.2001.2953
[4] Gabbay, D., I. Hodkinson, and M. Reynolds, Temporal Logic: Mathematical Foundations and Computational Aspects, Volume 1, Oxford University Press, 1994. · Zbl 0921.03023
[5] Goldblatt, R., Logics of Time and Computation, Number 7 in CSLI Lecture Notes, CSLI Publications, Stanford, 1987. · Zbl 0635.03024
[6] Litak, T., ’On notions of completeness weaker than Kripke completeness’, in Preliminary Proceedings of International Conference on AiML, Manchester, UK, 2004. · Zbl 1102.03065
[7] Ono, H., and A. Nakamura, ’On the size of refutation Kripke models for some linear modal and tense logics’, Studia Logica, 39:325–333, 1980. · Zbl 0466.03008 · doi:10.1007/BF00713542
[8] Prior, A., Past, Present and Future, Clarendon Press, Oxford, 1967. · Zbl 0169.29802
[9] Sistla, A., and E. Clarke, ’The complexity of propositional linear temporal logics’, Journal of the Association for Computing Machinery, 32:733–749, 1985. · Zbl 0632.68034
[10] Spaan, E., Complexity of Modal Logics. PhD thesis, Department of Mathematics and Computer Science, University of Amsterdam, 1993. · Zbl 0831.03005
[11] Wolter, F., ’Tense logic without tense operators’, Mathematical Logic Quarterly, 42:145–171, 1996. · Zbl 0858.03019 · doi:10.1002/malq.19960420113
[12] Zakharyaschev, M., and A. Alekseev, ’All finitely axiomatizable normal extensions of K4.3 are decidable’, Mathematical Logic Quarterly, 41:15–23, 1995. · Zbl 0818.03008 · doi:10.1002/malq.19950410103
[13] Zakharyaschev, M., F. Wolter, and A. Chagrov, ’AdvancedModal Logic’, in Handbook of Philosophical Logic, volume 3, Kluwer, 2nd edition, 2001, pp. 86–266. · Zbl 1003.03516
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.