×

On begins, meets and before. (English) Zbl 1259.03028

Summary: Interval temporal logics (ITLs) are logics for reasoning about temporal statements expressed over intervals, i.e., periods of time. The most famous temporal logic for intervals studied so far is probably Halpern and Shoham’s HS, which is the logic of the thirteen Allen’s interval relations. Unfortunately, HS and most of its fragments are undecidable. This discouraged the research in this area until recently, when a number non-trivial decidable ITLs have been discovered. This paper is a contribution towards the complete classification of all different fragments of HS. We consider here different combinations of the interval relations begins \((B)\), meets \((A)\), later \((L)\) and their inverses \(\bar A\), \(\bar B\) and \(\bar L\). We know from previous work that the combination \(AB\bar B \bar A\) is decidable only when finite domains are considered (and undecidable elsewhere), and that \(AB\bar B\) is decidable over the natural numbers. In the present paper we show that, over strongly discrete linear models (e.g. finite orders, the naturals, the integers), decidability of \(AB\bar B\) can be further extended to capture the language \(AB\bar B\bar L\), which lies strictly in between \(AB\bar B\) and \(AB\bar B \bar A\). The logic \(AB\bar B \bar L\) turns out to be maximal w.r.t decidability over the considered classes, and its satisfiability problem is EXPSPACE-complete. In this paper we also provide an optimal non-deterministic decision procedure, and we show that the language is powerful enough to polynomially encode metric constraints on the length of the current interval.

MSC:

03B44 Temporal logic
03B25 Decidability of theories and sets of sentences
68Q25 Analysis of algorithms and problem complexity
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] DOI: 10.1145/182.358434 · Zbl 0519.68079 · doi:10.1145/182.358434
[2] Bresolin D., Software and System Modeling · Zbl 1347.03032
[3] DOI: 10.1016/j.apal.2009.07.003 · Zbl 1221.03022 · doi:10.1016/j.apal.2009.07.003
[4] Goranko V., Journal of Universal Computer Science 9 pp 1137–
[5] DOI: 10.3166/jancl.14.9-54 · doi:10.3166/jancl.14.9-54
[6] Halpern J., Journal of the ACM 38 pp 279–
[7] Rabinovich A., Fundamenta Informaticae 42 pp 201–
[8] P. Van Emde Boas, Complexity, Logic and Recursion Theory, Lecture Notes in Pure and Applied Mathematics 187 (Marcel Dekker Inc., 1997) pp. 331–363.
[9] DOI: 10.1305/ndjfl/1093635589 · Zbl 0725.03006 · doi:10.1305/ndjfl/1093635589
[10] Zhou C., EATCS: Monographs in Theoretical Computer Science, in: Duration Calculus: A Formal Approach to Real-Time Systems (2004)
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.