General Verification Theories for Infinite-State Systems
The aim of the project is twofold, namely
- To give a unified explanation of existing decidability results for infinite-state systems, such as real-time automata, Petri nets, relational automata, and lossy channel systems.
- To provide guidelines for discovering similar decidability results for other classes of systems. The theory has been applied both by our group and by other research groups to provide new verification algorithms for timed Petri nets, timed networks, broadcast protocols, cache coherence protocols, etc.
We generalize the well-known technique of finite partitioning , where the state space of the original system is partitioned into a finite number of equivalence classes under bisimulation. Instead of an equivalence relation , we work with a preorder on the set of states. We generalize the conditions which finite partitioning methods impose on the system under consideration:
- the transition system is monotonic with respect to the preorder, i.e., transitions from larger states lead to larger states. This means that we work with a simulation rather than a bisimulation (larger states simulate smaller states). If the preorder is taken to be an equivalence relation, then the simulation reduces to a bisimulation.
- the preorder is a well quasi-ordering (WQO), which means that each infinite sequence contains an element which is larger than or equivalent to an earlier element in the sequence. If the preorder is taken to be an equivalence relation, then this condition amounts to finiteness of the number of equivalence classes.
- We have used thie methodology to explain several existing algorithms for verification of computation models such as real-time automata, Petri nets, relational automata, lossy channel systems etc. The methodology has also been used by our group and other research gropus to derive new verification algorithms for networks of timed processes, Timed petri nets, broadcast protocols, cache coherence protocols, etc. Better Quasi-Ordered Systems [ANa00, ANb00]
Many of the constraint systems derived according to the above method, suffer from a constraint explosion problem, as the number of the generated constraints grows exponentially with the size of the problem. In fact a refinement of the theory of well quasi-orderings, called the theory of better quasi-orderings (BQO) , seems to be more appropriate 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.
You can find here a list of our published work.