In automated verification of infinite-state systems, a variety of algorithms that operate on constraints representing sets of states have been developed. Many of these algorithms rely on well quasi-ordering of the constraint system for proving termination. A number of methods for generating new well quasi-ordered constraint systems have been proposed. However, many of these constraint systems suffer from constraint explosion as the number of constraints generated during analysis grows exponentially with the size of the problem. We suggest using the theory of better quasi-ordering to prove termination since that will allow generation of constraint systems that are less prone to constraint explosion. We also present a method to derive such constraint systems. We introduce existential zones, a constraint system for verification of systems with an unbounded number of clocks and use our methodology to prove that existential zones are better quasi-ordered. We show how to use existential zones in verification of timed Petri nets and present some experimental results. Finally, we present several other constraint systems which have been derived using our methodology.
Download BibTeX entry.