Skip to Main content Skip to Navigation
Journal articles

Verification of gap-order constraint abstractions of counter systems

Laura Bozzelli 1 Sophie Pinchinat 2 
2 S4 - System synthesis and supervision, scenarios
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : 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.
Document type :
Journal articles
Complete list of metadata
Contributor : Sophie Pinchinat Connect in order to contact the contributor
Submitted on : Monday, December 29, 2014 - 9:35:50 AM
Last modification on : Friday, February 4, 2022 - 3:18:29 AM

Links full text



Laura Bozzelli, Sophie Pinchinat. Verification of gap-order constraint abstractions of counter systems. Theoretical Computer Science, Elsevier, 2014, pp.36. ⟨10.1016/j.tcs.2013.12.002⟩. ⟨hal-01098739⟩



Record views