Parametrized Systems

At least two processes are in their critical sections is a typical example of such a constraint. The constraint specifies a minimal number of conditions to be satisfied by a configuration. Minimal condition constraints arise naturally when modelling parameterized systems. We have applied this framework to design verification algorithms for different classes of parameterized systems:

• Unordered systems with an unbounded number of real-valued clocks: for example networks of timed processes and timed Petri nets.
• Finite-state automata, operating on possibly unbounded data domains, ordered in an array, with local and global conditions as transitions' guard: communication via broadcast, rendez-vous and shared variables.

Minimal Condition Constraints can sometimes be seen as a special case of Regular Expressions. Regular Expressions, i.e automata, are used mainly in Regular Model Checking as the building blocs of a unifying framework for algorithmic verification of infinite-state systems with, e.g., queues, stacks, integers, or a parameterized topology. An important tool in Regular Model Checking is the ability to compute the transitive closure of a regular relation, i.e., the effect of arbitrarily long execution sequences. In the case of length preserving relations, we focus on two approaches: In the first one, Regular Model Checking the states are represented by strings over a finite alphabet; in the second one, Tree Regular Model Checking, is an extension of the first approach where states are represented by trees over a finite ranked alphabet and the transition relation by a bottom-up tree transducer.

We developed a simple and efficient framework for automatic verification of systems with a parametric number of communicating processes. The processes may be organized in various topologies such as words, multisets, rings, or trees.

Our method needs to inspect only a small number of processes in order to show correctness of the whole system. It relies on an abstraction function that views the system from the perspective of a fixed number of processes. The abstraction is used during the verification procedure in order to dynamically detect cut-off points beyond which the search of the state space need not continue.

We show that the method is complete for a large class of well quasi-ordered systems including Petri nets.
Our experimentation on a variety of benchmarks demonstrate that the method is highly efficient and that it works well even for classes of systems with undecidable verification problems. In particular, the method handles the fine-grained and full version of Szymanski's mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.