Propositional interval temporal logics are very expressive temporal logics, with simple syntax and semantics, which allow one to naturally express statements that refer to time intervals and continuous processes. Most of them feature temporal operators that only allow one to express properties of a single timeline. In this paper we develop a branching-time interval neighborhood logic that interleaves operators that quantify over possible timelines with operators that quantify over intervals belonging to a given timeline. We define its syntax and semantics, and we provide it with a doubly-exponential tableau-based decision procedure.

A tableau-based decision procedure for a branching-time interval temporal logic

BRESOLIN, Davide;
2005-01-01

Abstract

Propositional interval temporal logics are very expressive temporal logics, with simple syntax and semantics, which allow one to naturally express statements that refer to time intervals and continuous processes. Most of them feature temporal operators that only allow one to express properties of a single timeline. In this paper we develop a branching-time interval neighborhood logic that interleaves operators that quantify over possible timelines with operators that quantify over intervals belonging to a given timeline. We define its syntax and semantics, and we provide it with a doubly-exponential tableau-based decision procedure.
Logica temporale; logica ad intervalli; decidibiità; tableaux
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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/11562/312538
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact