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 A B and L. We know from previous work that the combination ABB A; is decidable only when finite domains are considered (and undecidable elsewhere), and that AB 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 B can be further extended to capture the language AB B L, which lies strictly in between AB B and AB B A. The logicAB B 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. © 2012 World Scientific Publishing Company.
On begins, meets and before
SCIAVICCO, Guido
2012
Abstract
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 A B and L. We know from previous work that the combination ABB A; is decidable only when finite domains are considered (and undecidable elsewhere), and that AB 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 B can be further extended to capture the language AB B L, which lies strictly in between AB B and AB B A. The logicAB B 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. © 2012 World Scientific Publishing Company.I documenti in SFERA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
