** Next:** Bibliography
** Up:** An Overview of MSR():
** Previous:** Applications

#

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]).

** Next:** Bibliography
** Up:** An Overview of MSR():
** Previous:** Applications
Giorgio Delzanno
2003-02-03