Related Works

Our work is inspired to the approach of [2,4], where existential regions are proposed as symbolic representation of configurations for parameterized Timed Petri Nets. In our framework we consider however problems and constraint systems that do not depend on the notion of time.

Networks of finite-state processes can be analyzed using the automata theoretic approach of [7,12,23], where sets of global states are represented as regular languages, and transitions as relations on languages. Symbolic exploration can then be performed using operations over automata with ad hoc accelerations or with automated abstractions techniques.

Differently from the automata theoretic approach, in our setting we handle parameterized systems in which individual components have local variables that range over unbounded values. The previous features also distinguish our approach from the verification with invisible invariants method of [5]. Contrary, we follow here the paradigm of symbolic model checking with rich assertional languages [23], trying to isolate decidable classes for which backward reachability terminates. The two approaches can be used to attack similar problems using different point-of-views.

Our ideas are related to previous works connecting Constraint Logic Programming and verification, see e.g. [16]. In this setting transition systems are encoded via CLP programs used to encode the global state of a system and its up.pngdates. We refine this idea by using multiset rewriting and constraints to locally specify up.pngdates to the global state. The notion of constrained multiset extends that of constrained atom of [16]. The locality of rules allows us to consider rich denotations (upward-closures) instead of flat ones (instances) like, e.g., in [16]. This way, we can lift the approach to the parameterized case.

Finally, the use of constraints, backward reachability, structural invariants and better quasi orderings seem all ingredients that distinguish our hybrid method from classical approaches based on multiset and AC rewriting techniques (see e.g. [11,26]).