## Ordered Counter-Abstraction: Refinable Subword Relations for Parameterized Verification

Pierre Ganty, Ahmed Rezine

We present an original refinable subword based
symbolic representation for the verification
of linearly ordered parameterized systems.
Such a system consists of arbitrary many finite processes placed in an array.
Processes communicate using global transitions
constrained by their relative positions (i.e., priorities).
The model can include binary communication, broadcast,
shared variables or dynamic creation and deletion of processes.
Configurations are finite words of arbitrary lengths.
The successful monotonic abstraction approach
uses the subword relation to define upward closed sets as
symbolic representations for such systems.
Natural and automatic refinements remained missing for such symbolic
representations.
For example, subword based relations (even in conjunction with
constraints on resulting Parikh images) are simply too coarse
for automatic forward verification of systems involving priorities.
We remedy to this situation and introduce a symbolic representation based on
an original combination of counter abstraction with subword
based relations.
This allows us to define an infinite family of relaxation operators
that guarantee termination by a new
well quasi ordering argument.
The proposed automatic analysis is
at least as precise and efficient
as monotonic abstraction when performed backwards.
It can also be successfully used in forward,
something monotonic abstraction is incapable of.
We implemented a prototype to illustrate the approach.

In Proceedings of
the 8th International Conference on Language and Automata Theory and Applications , LATA 2014
Madrid, Spain

Last version (pdf) 2014