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. The first definition of a general Well-Structured Transition System (WSTS) was introduced by Alain Finkel in his ICALP 1987 paper titled "A Generalization of the Procedure of Karp and Miller to Well Structured Transition Systems". WSTS decidability results can be applied to Petri nets, lossy channel systems, and more.