In computer science, specifically in the field of formal verification, well-structured transition systems 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 on a set is a quasi-orderingsuch that any infinite sequence of elements, from contains an increasing pair with. The set is said to be well-quasi-ordered, or shortly wqo. For our purposes, a transition system is a structure, where is any set, and . 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, such that
A well-structured system is a transition system with state set made up from a finite control state set, a data values set, furnished with a decidable pre-order which is extended to states by, which is well-structured as defined above and in addition has a computable set of minima for the set of predecessors of any upward closed subset of. 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,.
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 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, is there any transition path that leads from a given start state to a state ? An intuitive explanation for this question is: if 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, one typically considers an upward closed set of error states. The algorithm is based on the facts that in a well-quasi-order, any upward closed set has a finite set of minima, and any sequence of upward-closed subsets of converges after finitely many steps. The algorithm needs to store an upward-closed set 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 and computes at each iteration the set of immediate predecessors and adding it to the set. This iteration terminates after a finite number of steps, due to the property of well-quasi-orders. If is in the set finally obtained, then the output is "yes", otherwise it is "no".
