Metric Propositional Neighborhood Logic with an Equivalence Relation

The propositional interval logic of temporal neighborhood (PNL for short) features two modalities that make it possible to access intervals adjacent to the right (modality A) and to the left (modality Abar) of the current interval. PNL stands at a central position in the realm of interval temporal logics, as it is expressive enough to encode meaningful temporal conditions and decidable (undecidability rules over interval temporal logics, while PNL is NEXPTIME-complete). Moreover, it is expressively complete with respect to FO2[<]. Various extensions of PNL have been studied in the literature, including metric, hybrid, and first-order ones. Here, we study the effects of the addition of an equivalence relation sim to Metric PNL (MPNLsim). We first show that finite satisfiability for PNL extended with sim is still NEXPTIME-complete. Then, we prove that finite satisfiability for MPNLsim can be reduced to the decidable 0-0 reachability problem for vector addition systems and vice versa (EXPSPACE-hardness immediately follows).