Well-structured transition system

In computer science, specifically in the field of formal verification, well-structured transition systems (WSTSs) 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 formula_1 on a set formula_2 is a quasi-ordering (i.e., a preorder or reflexive, transitive binary relation) such that any infinite sequence of elements formula_3, from formula_2 contains an increasing pair formula_5 with formula_6. The set formula_2 is said to be well-quasi-ordered, or shortly wqo.
For our purposes, a "transition system" is a structure formula_8, where formula_9 is any set (its elements are called "states"), and formula_10 (its elements are called "transitions"). In general a transition system may have additional structure like initial states, labels on transitions, accepting states, etc. (indicated by the dots), but they do not concern us here.
A well-structured transition system consists of a transition system formula_11, such that
Well-structured systems.
A well-structured system is a transition system formula_24 with state set formula_25 made up from a finite "control state" set formula_26, a "data values" set formula_27, furnished with a "decidable" pre-order formula_28 which is extended to states by formula_29, which is well-structured as defined above (formula_14 is monotonic, i.e. upward compatible, with respect to formula_31) and in addition has a "computable" set of minima for the set of predecessors of any upward closed subset of formula_9.
Well-structured systems adapt the theory of well-structured transition systems for modelling certain classes of systems encountered in computer science and provide the basis for decision procedures to analyse such systems, hence the supplementary requirements: the definition of a WSTS itself says nothing about the computability of the relations formula_31, formula_14.
Uses in Computer Science.
Well-structured Systems.
Coverability can be decided for any well-structured system, and so can reachability of a given control state, by the "backward algorithm" of Abdulla et al. or for specific subclasses of well-structured systems (subject to strict monotonicity, e.g. in the case of unbounded Petri nets) by a forward analysis based on a Karp-Miller coverability graph.
Backward Algorithm.
The backward algorithm allows the following question to be answered: given a well-structured system and a state formula_35, is there any transition path that leads from a given start state formula_36 to a state formula_37 (such a state is said to "cover" formula_35)?
An intuitive explanation for this question is: if formula_35 represents an error state, then any state "containing" it should also be regarded as an error state. If a well-quasi-order can be found that models this "containment" of states and which also fulfills the requirement of monotonicity with respect to the transition relation, then this question can be answered.
Instead of one minimal error state formula_35, one typically considers an upward closed set formula_41 of error states.
The algorithm is based on the facts that in a well-quasi-order formula_42, any upward closed set has a finite set of minima, and any sequence formula_43 of upward-closed subsets of formula_44 converges after finitely many steps (1).
The algorithm needs to store an upward-closed set formula_45 of states in memory, which it can do because an upward-closed set is representable as a finite set of minima. It starts from the upward closure of the set of error states formula_41 and computes at each iteration the (by monotonicity also upward-closed) set of immediate predecessors and adding it to the set formula_45. This iteration terminates after a finite number of steps, due to the property (1) of well-quasi-orders. If formula_36 is in the set finally obtained, then the output is "yes" (a state of formula_41 can be reached), otherwise it is "no" (it is not possible to reach such a state).