Satisfiability of ECTL⁎ with constraints.

Satisfiability for ECTL* with local constraints over the integers is decidable.Finite satisfiability for ECTL* with local constraints over the integers is decidable.Locality of the constraints is necessary for decidability. We show that satisfiability and finite satisfiability for ECTL * with equality-, order-, and modulo-constraints over Z are decidable. Since ECTL * is a proper extension of CTL * this greatly improves the previously known decidability results for certain fragments of CTL * , e.g., the existential and positive fragments and EF. We also show that our choice of local constraints is necessary for the result in the sense that, if we add the possibility to state non-local constraints over Z , the resulting logic becomes undecidable.