Well-structured transition systems are a class of computational models where the infinite state space is subject to a well-quasi-ordering respected by the transition rules. As a result, some verification problems are decidable, but the decision problems fall in very large complexity classes that must be described with the fast-growing hierarchy.
A transition system is defined by a set of states \(S\) and a transition table, a binary relation \(\rightarrow\) over \(S\). We use \(\rightarrow^*\) to denote the reflexive transitive closure of \(\rightarrow\). A well-structured transition system equips a transition system with another binary relation \(\leq\) such that \(\leq\) well-quasi-orders \(S\), and the following is true: for all \(s_1, t_1, s_2 \in S\) such that \(s_1 \leq t_1\) and \(s_1 \rightarrow s_2\), there is a \(t_2 \in S\) such that \(s_2 \leq t_2\) and \(t_1 \rightarrow^* t_2\).