Ordered Counter-Abstraction
We introduce a new symbolic representation based on an original
generalization of counter abstraction. Unlike classical counter abstraction
(used in the analysis of parameterized systems with unordered or unstructured
topologies) the new representation is tailored for proving properties of
linearly ordered parameterized systems, i.e., systems with arbitrary many
finite processes placed in an array. The relative positions in the array
capture the relative priorities of the processes. Configurations of such
systems are finite words of arbitrary lengths. The processes communicate using
global transitions constrained by their relative priorities. Intuitively, an
element of the symbolic representation has a base and a set of counters. It
denotes configurations that respect the constraints imposed by the counters and
that have the base as a sub word. We use the new representation in a uniform
and automatic Counter Example Guided Refinement scheme. We introduce a
relaxation operator that allows a well quasi ordering argument for the
termination of each iteration of the refinement loop. We explain how to refine
the relaxation to systematically prune out false positives. We implemented a
tool to illustrate the approach on a number of parameterized systems.
Published in \url{http://arxiv.org/abs/1204.0131},
Last version (pdf) 2012