Authors: Pierre Ganty, Ahmed Rezine
Abstract: 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 and 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 instance, subword based relations 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 upper closure operators on the new symbolic representations. Each operator allows us to approximate reachable states using symbolic representations where termination is guaranteed by a new well quasi ordering argument. We propose a generic counter example based refinement scheme that builds on these symbolic representations. The proposed automatic analysis is at least as precise and efficient as monotonic abstraction when performed backwards. It can also be used in forward, something monotonic abstraction is incapable of. We implemented a prototype to support the previous claims.
Submitted as an invited journal version
Working version (pdf) 2014