Well quasi orders are a key ingredient in several algorithmic or structural results. For counter systems, the most often used wqo is $(\mathbb{N}^k,\leq)$, but finite sequences cum embeddings and even tree structures also appear: when dealing with infinite-state systems, Dickson's Lemma, Higman's Lemma and Kruskal's Tree Theorem are tools of the verification trade. For instance, both the approaches of Mayr (1981) and Leroux (2011) rely on such a termination argument in their proofs of decidability of the reachability problem in vector addition systems.

In verification, wqo's are seen as abstract results without much computational content. Thus verification researchers do not know how to develop any meaningful complexity analysis of results based on wqo theory. A little-exploited fact is that typical uses of wqo's, where the elements are constructed by some well identified process with a controlled complexity, yield complexity upper bounds. Such investigations started in the field of Petri nets (McAloon, 1984; Clote, 1986) for Dickson's Lemma and were further studied in that of rewriting systems---see e.g. Cichoń and Tahhan Bittar (1998) for Higman's Lemma and Weiermann (1994) for Kruskal's Tree Theorem. A typical result in this area is to majorize the complexity, seen as a function of the input size, by some function in a subrecursive hierarchy, like the Fast Growing Hierarchy.

However, the main positive results for well-structured systems (WSTS) were not provided with any complexity analysis until (Schnoebelen, 2002; Schnoebelen, 2010; Chambart and Schnoebelen, 2008) opened the way. There are two reasons for this state of affairs: first the relevant complexity classes (based on ordinal-recursive hierarchies) are unusual hence mostly unknown in verification, secondly the existing literature on upper bounds, starting with (McAloon, 1984), is scarce and difficult to read for potential users.

Two recent contributions (Figueira et al, 2011; Schmitz and Schnoebelen, 2011) present simplified proofs of the upper bounds of (McAloon, 1984; Cichoń and Tahhan Bittar, 1998) and open the way to new results, and we can hope to provide complexity upper bounds for the algorithms of Mayr (1981) and Leroux (2011) by extending their approach.