Well (and Better) Quasi-Ordered Transition Systems

In this paper, we give a step by step introduction to the theory ofwell quasi-orderedtransition systems. The framework combines two concepts, namely (i) transition systems which aremonotonicwrt. awell-quasi ordering; and (ii) a scheme for symbolicbackwardreachability analysis. We describe several models with infinite-state spaces, which can be analyzed within the framework, e.g., Petri nets, lossy channel systems, timed automata, timed Petri nets, and multiset rewriting systems. We will also presentbetter quasi-orderedtransition systems which allow the design of efficient symbolic representations of infinite sets of states.