Well-structured transition system

In computer science, specifically in the field of formal verification, well-structured transition systems (WSTS's) are a general class of infinite state systems for which many verification problems are decidable, owing to the existence of a kind of order between the states of the system which is compatible with the transitions of the system. WSTS decidability results can be applied to Petri nets, lossy channel systems, and more.

Formal definition

Recall that a well-quasi-ordering $\leq$ on a set $X$ is a quasi-ordering (i.e., a reflexive, transitive binary relation) such that any infinite sequence of elements $x_{0},x_{1},x_{2},\ldots$ , from $X$ contains an increasing pair $x_{i}\leq x_{j}$ with $i<j$ . The set $X$ is said to be well-quasi-ordered, or shortly wqo.

For our purposes, a transition system is a structure ${\mathcal {S}}=\langle S,\rightarrow ,\cdots \rangle$ , where $S$ is any set (its elements are called states), and $\rightarrow \subseteq S\times S$ (its elements are called transitions). In general a transition system may have additional structure like initial states, labels on transitions, accepting states, etc, but they do not concern us here.

A well-structured transition system consists of a transition system $\langle S,\to ,\leq \rangle$ , such that

$\leq \subseteq S\times S$ is a well-quasi-ordering on the set of states.
$\leq$ is upward compatible with $\to$ : that is, for all transitions $s_{1}\to s_{2}$ (by this we mean $(s_{1},s_{2})\in \to$ ) and for all $t_{1}$ such that $s_{1}\leq t_{1}$ , there exists $t_{2}$ such that $t_{1}{\xrightarrow {*}}t_{2}$ (that is, $t_{2}$ can be reached from $t_{1}$ by a sequence of zero or more transitions) and $s_{2}\leq t_{2}$ .