Verification of gap-order constraint abstractions of counter systems

We investigate verification problems for gap-order constraint systems   (GCSGCS), an (infinitely-branching) abstract model of counter machines, in which constraints (over ZZ) between the variables of the source state and the target state of a transition are gap-order constraints   (GCGC) [32]. GCSGCS extend monotonicity constraint systems [7], integral relation automata [16], and constraint automata in [19]. First, we address termination and fairness analysis of GCSGCS. Since GCSGCS are infinitely-branching, termination does not imply strong termination  , i.e. the existence of an upper bound on the lengths of the runs from a given state. We show that the termination problem, the strong termination problem, and the fairness problem for GCSGCS (the latter consisting in checking the existence of infinite runs in GCSGCS satisfying acceptance conditions à la Büchi) are decidable and Pspace-complete. Moreover, for each control location of the given GCSGCS, one can build a GCGC representation of the set of counter variable valuations from which termination (resp., strong termination, resp., fairness) does not hold (resp., does not hold, resp., does hold).Next, we consider a constrained branching-time logic, GCCTL⁎GCCTL⁎, obtained by enriching CTL⁎CTL⁎ with GCGC, thus enabling expressive properties and subsuming the setting of [16]. We establish that, while model-checking GCSGCS against the universal fragment of GCCTL⁎GCCTL⁎ is undecidable, model-checking against the existential fragment, and satisfiability of both the universal and existential fragments are instead decidable and Pspace-complete (note that the two fragments are not dual since GCGC are not closed under negation). Moreover, our results imply Pspace-completeness of known verification problems that were shown to be decidable in [16] with no elementary upper bounds.