\input zb-basic
\input zb-ioport
\iteman{io-port 06046573}
\itemau{Bozzelli, Laura; Pinchinat, Sophie}
\itemti{Verification of gap-order constraint abstractions of counter systems.}
\itemso{Kuncak, Viktor (ed.) et al., Verification, model checking, and abstract interpretation. 13th international conference, VMCAI 2012, Philadelphia, PA, USA, January 22--24, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-27939-3/pbk). Lecture Notes in Computer Science 7148, 88-103 (2012).}
\itemab
Summary: We investigate verification problems for gap-order constraint systems (GCS), an (infinitely-branching) abstract model of counter machines, in which constraints (over $\Bbb Z)$ 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 \`a la B\"uchi (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.
\itemrv{~}
\itemcc{}
\itemut{}
\itemli{doi:10.1007/978-3-642-27940-9\_7}
\end