In this paper, we give a step by step introduction
to the theory of well quasi-ordered transition systems.
The framework combines two concepts, namely
(i) transition systems which are monotonic wrt. a well-quasi ordering; and
(ii) a scheme for symbolic backward reachability 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 present better quasi-ordered transition systems
which allow the design of efficient symbolic representations of infinite sets
of states.