Adding two equivalence relations to the interval temporal logic AB

The interval temporal logic AB features two modalities that make it possible to access intervals which are adjacent to the right of the current interval (modality (A)) and proper subintervals that have the same left endpoint of it (modality 〈B〉). AB is one of the most significant interval logics, as it allows one to express meaningful (metric) properties, while maintaining decidability (undecidability rules over interval logics, AB is EXPSPACE-complete [14]). In an attempt to capture ωS-regular languages with interval logics [15], it was proved that AB extended with an equivalence relation, denoted AB ∼, is decidable (non-primitive recursive) on the class of finite linear orders and undecidable on ℕ. The question whether the addition of two or more equivalence relations makes finite satisfiability for AB undecidable was left open. In this paper, we answer this question proving that AB∼1∼2 is undecidable.