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.[1] 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.

Definition Edit

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\).

Sources Edit


Ad blocker interference detected!

Wikia is a free-to-use site that makes money from advertising. We have a modified experience for viewers using ad blockers

Wikia is not accessible if you’ve made further modifications. Remove the custom ad blocker rule(s) and the page will load as expected.