Abstract
Decidability and complexity of the satisfiability problem for the logics of time intervals have been extensively studied in the recent years. Even though most interval logics turn out to be undecidable, meaningful exceptions exist, such as the logics of temporal neighborhood and (some of) the logics of the subinterval relation. In this paper, we explore a different path to decidability: instead of restricting the set of modalities or imposing severe semantic restrictions, we take the most expressive interval temporal logic studied so far, namely, Venema’s CDT, and we suitably limit the negation depth of modalities. The decidability of the satisfiability problem for the resulting fragment, called CDTBS, over the class of all linear orders, is proved by embedding it into a well-known decidable quantifier prefix class of first-order logic, namely, Bernays-Schönfinkel class. In addition, we show that CDTBS is in fact NP-complete (Bernays-Schönfinkel class is NEXPTIME-complete), and we prove its expressive completeness with respect to a suitable fragment of Bernays-Schönfinkel class. Finally, we show that any increase in the negation depth of CDTBS modalities immediately yields undecidability.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Allen, J.: Maintaining knowledge about temporal intervals. Commun. ACM 26(11), 832–843 (1983)
Andréka, H., van Benthem, J., Németi, I.: Back and forth between modal logic and classical logic. Log. J. IGPL 3(5), 685–720 (1995)
Benthem, J.V., Thomason, S.K.: Dynamic bits and pieces. Report LP-97-01, ILLC, University of Amsterdam (1997)
Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Springer (1999)
Bresolin, D., Della Monica, D., Goranko, V., Montanari, A., Sciavicco, G.: Decidable and undecidable fragments of Halpern and Shoham’s interval temporal logic: towards a complete classification. In: Proc. of LPAR’08. LNCS, vol. 5330, pp. 590–604. Springer (2008)
Bresolin, D., Della Monica, D., Goranko, V., Montanari, A., Sciavicco, G.: Undecidability of interval temporal logics with the overlap modality. In: Proc. of TIME’09, pp. 88–95. IEEE Comp. Society (2009)
Bresolin, D., Della Monica, D., Goranko, V., Montanari, A., Sciavicco, G.: Metric propositional neighborhood logics. J. Soft. Syst. Mod. (2012). doi:10.1007/s10270-011-0195-y
Bresolin, D., Goranko, V., Montanari, A., Sciavicco, G.: Propositional interval neighborhood logics: expressiveness, decidability, and undecidable extensions. Ann. Pure Appl. Logic 161(3), 289–304 (2009)
Bresolin, D., Montanari, A., Sala, P., Sciavicco, G.: Optimal tableaux for right propositional neighborhood logic over linear orders. In: Proc. of JELIA’08. LNAI, vol. 5293, pp. 62–75. Springer (2008)
Bresolin, D., Montanari, A., Sala, P., Sciavicco, G.: What’s decidable about Halpern and Shoham’s interval logic? The maximal fragment \(\mathsf{AB \overline{BL}}\). In: Proc. of LICS’11, pp. 387–396. IEEE Comp. Society Press (2011)
Della Monica, D., Goranko, V., Montanari, A., Sciavicco, G.: Expressiveness of the interval logics of allen’s relations on the class of all linear orders: complete classification. In: Proc. of IJCAI’11, pp. 845–850 (2011)
Etessami, K., Vardi, M.Y., Wilke, T.: First-order logic with two variables and unary temporal logic. Inf. Comput. 179(2), 279–295 (2002)
Gabbay, D., Hodkinson, I., Reynolds, M.: Temporal Logic: Mathematical Foundations and Computational Aspects. Oxford University Press (1994)
Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proc. of POPL’80, pp. 163–173. ACM Press (1980)
Goranko, V., Montanari, A., Sala, P., Sciavicco, G.: A general tableau method for propositional interval temporal logics: theory and implementation. Journal of Applied Logic 4(3), 305–330 (2006)
Goranko, V., Montanari, A., Sciavicco, G.: Propositional interval neighborhood temporal logics. J. Univers. Comput. Sci. 9(9), 1137–1167 (2003)
Goranko, V., Montanari, A., Sciavicco, G.: A road map of interval temporal logics and duration calculi. Applied Non-Classical Logics 14(1–2), 9–54 (2004)
Halpern, J., Shoham, Y.: A propositional modal logic of time intervals (short version). In: Proc. of LICS’86, pp. 279–292. IEEE Comp. Society (1986)
Halpern, J.Y., Shoham, Y.: A propositional modal logic of time intervals. J. ACM 38, 935–962 (1991)
Hodkinson, I., Montanari, A., Sciavicco, G.: Non-finite axiomatizability and undecidability of interval temporal logics with C, D, and T. In: Proc. of CSL’08. LNCS, vol. 5213, pp. 308–322. Springer (2008)
Immerman, N., Kozen, D.: Definability with bounded number of bound variables. Inf. Comput. 83(2), 121–139 (1989)
Kamp, H.: Events, instants and temporal reference. In: Semantics from Different Points of View, pp. 27–54. Springer (1979)
Marcinkowski, J., Michaliszyn, J.: The ultimate undecidability result for the Halpern-Shoham logic. In: Proc. of LICS’11, pp. 377–386. IEEE Comp. Society Press (2011)
Marcinkowski, J., Michaliszyn, J., Kieronski, E.: B and D are enough to make the Halpern-Shoham logic undecidable. In: Proc. of ICALP’10—Part II. LNCS, vol. 6199, pp. 357–368. Springer (2010)
Montanari, A., Peron, A., Policriti, A.: Extending Kamp’s theorem to model time granularity. J. Log. Comput. 12(4), 641–678 (2002)
Montanari, A., Puppis, G., Sala, P.: A decidable spatial logic with cone-shaped cardinal directions. In: Proc. of CSL’09. LNCS, vol. 5771, pp. 394–408. Springer (2009)
Montanari, A., Puppis, G., Sala, P.: A Decidable Spatial Logic with Cone-Shape Cardinal Directions. Research Report 3, Dipartimento di Matematica ed Informatica, Università di Udine (2010)
Montanari, A., Puppis, G., Sala, P.: Maximal decidable fragments of Halpern and Shoham’s modal logic of intervals. In: Proc. of ICALP’10—Part II. LNCS, vol. 6199, pp. 345–356. Springer (2010)
Montanari, A., Puppis, G., Sala, P., Sciavicco, G.: Decidability of the interval temporal logic \(AB\bar{B}\) on natural numbers. In: Proc. of STACS’10, pp. 597–608 (2010)
Otto, M.: Two variable first-order logic over ordered domains. J. Symb. Log. 66(2), 685–702 (2001)
Szwast, W., Tendera, L.: The guarded fragment with transitive guards. Ann. Pure Appl. Logic 128(1–3), 227–276 (2004)
Venema, Y.: Expressiveness and completeness of an interval tense logic. Notre Dame J. Form. Log. 31(4), 529–547 (1990)
Venema, Y.: A modal logic for chopping intervals. J. Log. Comput. 1(4), 453–476 (1991)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Bresolin, D., Della Monica, D., Montanari, A. et al. The light side of interval temporal logic: the Bernays-Schönfinkel fragment of CDT. Ann Math Artif Intell 71, 11–39 (2014). https://doi.org/10.1007/s10472-013-9337-y
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10472-013-9337-y