Decidability and complexity of the satisfiability problem for the logics of time intervals have been extensively studied in the last years. Even though most interval logics turnout 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 suitable semantic restrictions, we take the most expressive interval temporal logic studied so far, namely, Venema's CDT, and we suitably limit the nesting degree of modalities. The decidability of the satisfiability problem for the resulting CDT fragment is proved by embedding it into a well-known decidable prefix quantifier class of first-order logic, namely, the Bernays-Schonfinkel's class. In addition, we show that such a fragment is in fact NP-complete (theBernays-Schonfinkel's class is NEXPTIME-complete), and that any natural extension of it is undecidable.

The light side of Interval Temporal Logic: the Bernays-Schoenfinkel's fragment of CDT / D. Bresolin; D. Della Monica; A. Montanari; G. Sciavicco. - STAMPA. - (2011), pp. 123-130. (Intervento presentato al convegno TIME 2011: 18th International Symposium on Temporal Representation and Reasoning tenutosi a Lubecca, Germania nel Settembre 2011) [10.1109/TIME.2011.20].

The light side of Interval Temporal Logic: the Bernays-Schoenfinkel's fragment of CDT

BRESOLIN, DAVIDE;
2011

Abstract

Decidability and complexity of the satisfiability problem for the logics of time intervals have been extensively studied in the last years. Even though most interval logics turnout 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 suitable semantic restrictions, we take the most expressive interval temporal logic studied so far, namely, Venema's CDT, and we suitably limit the nesting degree of modalities. The decidability of the satisfiability problem for the resulting CDT fragment is proved by embedding it into a well-known decidable prefix quantifier class of first-order logic, namely, the Bernays-Schonfinkel's class. In addition, we show that such a fragment is in fact NP-complete (theBernays-Schonfinkel's class is NEXPTIME-complete), and that any natural extension of it is undecidable.
2011
TIME 2011: 18th International Symposium on Temporal Representation and Reasoning
123
130
The light side of Interval Temporal Logic: the Bernays-Schoenfinkel's fragment of CDT / D. Bresolin; D. Della Monica; A. Montanari; G. Sciavicco. - STAMPA. - (2011), pp. 123-130. (Intervento presentato al convegno TIME 2011: 18th International Symposium on Temporal Representation and Reasoning tenutosi a Lubecca, Germania nel Settembre 2011) [10.1109/TIME.2011.20].
D. Bresolin; D. Della Monica; A. Montanari; G. Sciavicco
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/371962
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact