extended with atomic formulas built over a constraint language interpreting variables in ℤ has been shown to have a decidable satisfiability and model-checking problem. This language allows to compare the variables at different states of the model and include periodicity constraints, comparison constraints, and a restricted form of quantification. On the other hand, the
counterpart of this logic (and hence also its
counterpart which subsumes both
) has an undecidable model-checking problem. In this paper, we substantially extend the decidability border, by considering a meaningful fragment of
extended with such constraints (which subsumes both the universal and existential fragments, as well as the
-like fragment) and show that satisfiability and model-checking over relational automata that are abstraction of counter machines are decidable. The correctness and the termination of our algorithm rely on a suitable well quasi-ordering defined over the set of variable valuations.