Adding an equivalence relation to the interval logic ABBbar: complexity and expressiveness

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 ABBbar of Allen’s relations meets, begun by, and begins.We first prove that the satisfiability problem for the resulting logic ABBbarTilde remains decidable over finite linear orders, but it becomes nonprimitive recursive, while decidability is lost over N.. We also show that decidability over N can be recovered by restricting to a suitable subset of models. Then, we show that ABBbarTilde s expressive enough to define omegaS-regular languages, thus establishing a promising connection between interval temporal logics and extended omega-regular languages.