Interval temporal logics provide a general framework for temporal representation and reasoning, where classical (point-based) linear temporal logics can be recovered as special cases. In this paper, we study the effects of the addition of an equivalence relation to one of the most representative interval temporal logics, namely, the logic ABB̅ of Allen's relations meets, begun by, and begins. We first prove that the satisfiability problem for the resulting logic ABB̅ ℕ remains decidable over finite linear orders, but it becomes nonprimitive recursive, while decidability is lost over N. We also show that decidability over can be recovered by restricting to a suitable subset of models. Then, we show that ABB̅ ℕ is expressive enough to define ωS-regular languages, thus establishing a promising connection between interval temporal logics and extended ω-regular languages.
Adding an Equivalence Relation to the Interval Logic ABB: Complexity and Expressiveness
SALA, Pietro
2013-01-01
Abstract
Interval temporal logics provide a general framework for temporal representation and reasoning, where classical (point-based) linear temporal logics can be recovered as special cases. In this paper, we study the effects of the addition of an equivalence relation to one of the most representative interval temporal logics, namely, the logic ABB̅ of Allen's relations meets, begun by, and begins. We first prove that the satisfiability problem for the resulting logic ABB̅ ℕ remains decidable over finite linear orders, but it becomes nonprimitive recursive, while decidability is lost over N. We also show that decidability over can be recovered by restricting to a suitable subset of models. Then, we show that ABB̅ ℕ is expressive enough to define ωS-regular languages, thus establishing a promising connection between interval temporal logics and extended ω-regular languages.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
