Abstract
We introduce and investigate a number of fragments of propositional temporal logic LTL over the flow of time (ℤ, <). The fragments are defined in terms of the available temporal operators and the structure of the clausal normal form of the temporal formulas. We determine the computational complexity of the satisfiability problem for each of the fragments, which ranges from NLogSpace to PTime, NP and PSpace.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Apostol, T.: Introduction to Analytic Number Theory. Springer (1976)
Artale, A., Calvanese, D., Kontchakov, R., Ryzhikov, V., Zakharyaschev, M.: Reasoning over extended ER models. In: Parent, C., Schewe, K.-D., Storey, V.C., Thalheim, B. (eds.) ER 2007. LNCS, vol. 4801, pp. 277–292. Springer, Heidelberg (2007)
Artale, A., Calvanese, D., Kontchakov, R., Zakharyaschev, M.: The DL-Lite family and relations. Journal of Artificial Intelligence Research 36, 1–69 (2009)
Artale, A., Kontchakov, R., Ryzhikov, V., Zakharyaschev, M.: Past and future of DL-Lite. In: Proc. of AAAI, pp. 243–248 (2010)
Artale, A., Kontchakov, R., Ryzhikov, V., Zakharyaschev, M.: Complexity of reasoning over temporal data models. In: Parsons, J., Saeki, M., Shoval, P., Woo, C., Wand, Y. (eds.) ER 2010. LNCS, vol. 6412, pp. 174–187. Springer, Heidelberg (2010)
Artale, A., Kontchakov, R., Ryzhikov, V., Zakharyaschev, M.: The Complexity of Clausal Fragments of LTL. CoRR abs/1306.5088 (2013)
Bauland, M., Schneider, T., Schnoor, H., Schnoor, I., Vollmer, H.: The complexity of generalized satisfiability for linear temporal logic. Logical Methods in Computer Science 5(1) (2009)
Berardi, D., Calvanese, D., De Giacomo, G.: Reasoning on UML class diagrams. Artificial Intelligence 168(1-2), 70–118 (2005)
Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: Tractable reasoning and efficient query answering in description logics: The DL-Lite family. Journal of Automated Reasoning 39(3), 385–429 (2007)
Chen, C.-C., Lin, I.-P.: The computational complexity of satisfiability of temporal Horn formulas in propositional linear-time temporal logic. Information Processing Letters 45(3), 131–136 (1993)
Chrobak, M.: Finite automata and unary languages. Theoretical Computer Science 47(2), 149–158 (1986)
Demri, S., Schnoebelen, P.: The complexity of propositional linear temporal logics in simple cases. Information and Computation 174(1), 84–103 (2002)
Dixon, C., Fisher, M., Konev, B.: Tractable temporal reasoning. In: Proc. of IJCAI, pp. 318–323 (2007)
Fisher, M.: A resolution method for temporal logic. In: Proc. of IJCAI, pp. 99–104. Morgan Kaufmann (1991)
Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Transactions on Computational Logic 2(1), 12–56 (2001)
Gabbay, D., Hodkinson, I., Reynolds, M.: Temporal Logic: Mathematical Foundations and Computational Aspects, vol. 1. Oxford University Press (1994)
Gabbay, D., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-dimensional modal logics: theory and applications. Elsevier (2003)
Halpern, J., Reif, J.: The propositional dynamic logic of deterministic, well-structured programs. In: Proc. of FOCS, pp. 322–334. IEEE (1981)
Lichtenstein, O., Pnueli, A., Zuck, L.D.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 196–218. Springer, Heidelberg (1985)
Lutz, C., Wolter, F., Zakharyaschev, M.: Temporal description logics: A survey. In: Proc. of TIME, pp. 3–14. IEEE Comp. Society (2008)
Markey, N.: Past is for free: On the complexity of verifying linear temporal properties with past. Acta Informatica 40(6-7), 431–458 (2004)
Ono, H., Nakamura, A.: On the size of refutation Kripke models for some linear modal and tense logics. Studia Logica 39, 325–333 (1980)
Plaisted, D.: A decision procedure for combinations of propositional temporal logic and other specialized theories. Journal of Automated Reasoning 2, 171–190 (1986)
Rabinovich, A.: Temporal logics over linear time domains are in PSPACE. In: Kučera, A., Potapov, I. (eds.) RP 2010. LNCS, vol. 6227, pp. 29–50. Springer, Heidelberg (2010)
Reynolds, M.: The complexity of decision problems for linear temporal logics. Journal of Studies in Logic 3(1), 19–50 (2010)
Sistla, A., Clarke, E.: The complexity of propositional linear temporal logics. In: Proc. of STOC, pp. 159–168. ACM (1982)
Stockmeyer, L., Meyer, A.: Word problems requiring exponential time: Preliminary report. In: Proc. of STOC, pp. 1–9. ACM (1973)
To, A.W.: Unary finite automata vs. arithmetic progressions. Information Processing Letters 109(17), 1010–1014 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Artale, A., Kontchakov, R., Ryzhikov, V., Zakharyaschev, M. (2013). The Complexity of Clausal Fragments of LTL. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2013. Lecture Notes in Computer Science, vol 8312. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-45221-5_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-45221-5_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-45220-8
Online ISBN: 978-3-642-45221-5
eBook Packages: Computer ScienceComputer Science (R0)