FANDOM

10,825 Pages

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

1. http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FinSch-TCS99.pdf