Verification of Gap-Order Constraint Abstractions of Counter Systems

We investigate verification problems for

gap-order constraint systems

(

GCS

), an (infinitely-branching) abstract model of counter machines, in which constraints (over ℤ) between the variables of the source state and the target state of a transition are

gap-order constraints

(

GC

) [27].

GCS

extend monotonicity constraint systems [5], integral relation automata [12], and constraint automata in [15]. First, we show that checking the existence of infinite runs in

GCS

satisfying acceptance conditions à la Büchi (fairness problem) is decidable and

Pspace

-complete. Next, we consider a constrained branching-time logic,

GCCTL*

, obtained by enriching

CTL*

with

GC

, thus enabling expressive properties and subsuming the setting of [12]. We establish that, while model-checking

GCS

against the universal fragment of

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

GC

are not closed under negation). Moreover, our results imply

Pspace

-completeness of the verification problems investigated and shown to be decidable in [12], but for which no elementary upper bounds are known.