Department of Information Technology

Efficient Algorithms

Several highly nontrivial algorithms have been designed for verification of infinite-state systems such as timed automata, lossy channel systems, (unbounded) Petri nets, broadcast protocols, relational automata, parametrized systems, etc. These methods operate on symbolic representations, called constraints each of which may represent an infinite set of states. However, many of these algorithms suffer from a constraint explosion as the number of generated constraints grows exponentially with the parameters of the system. This problem is similar to the state explosion encountered in verification of finite-state systems. As the interest in the area of infinite-state systems increases, it will be important to design tools which limit the impact of constraint explosion.

Contributions

We have considered several methods to combat the constraint explosion problem. These methods aim either at reducing the number of constarints which need to be analysed (partial order and unfoldings) or at producing more compact constraint systems (better quasi-orderings).

The technique of net unfoldings has been applied by Esparza, McMillan, and others for efficient verification of finite-state systems. In this project, we extend the application of unfoldings to the context of infinite state systems. We adapt an algorithm for backward reachability analysis, developed within the project on general theories for infinite-state stystems (see here ). Instead of working on individual states (as is the case with the previous approaches to unfoldings) we let our unfolding algorithm operate on constraints each of which may represent an (infinite) set of states. We perform backward reachability analysis and compute a postfix of the unfolding, which gives a complete characterization of the set of states from which we can reach a final marking. Using concepts from the theory of well quasi-orderings we show that the postfix is always finite.

In a similar manner to unfoldings, we have developed a methodology for lifting partial order reductions fto symbolic verification. The method is equally applicable to the verification of finite-state and infinite-state systems. It considers methods that check safety properties, either by forward reachability analysis or by backward reachability analysis. We base the method on the concept of commutativity (in one direction) between predicate transformers. Since the commutativity relation is not necessarily symmetric, this generalizes those existing approaches to partial order verification which are based on a symmetric dependency relation. we have applied the method to lossy channel systems and to (unbounded) Petri nets.

  • Better Quasi-Ordered Constraint Systems [ANa00, ANb00]

A refinement of the theory of well quasi-orderings, called the theory of better quasi-orderings (BQO) , shows to be more suitable for verification of infinite-state systems. The main advantage of BQOs is that they are closed under disjunction, which allows to work with much more compact constraint systems. We have applied BQOs to derive new compact constraint systems for verification of systems with unboundedly many clocks, broadcast protocols, lossy channel systems, and integral relational automata.

Publications

You can find here a list of our published work.

Updated  2007-04-23 19:43:07 by Ahmed Rezine.