Algorithmic Theory of WQOs

Well quasi orders are a key ingredient in several algorithmic or structural results. For counter systems, the most often used 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, 's are seen as abstract results without much computational content. Thus verification researchers do not know how to develop any meaningful analysis of results based on theory. A little-exploited fact is that typical uses of '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 (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 , 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 () were not provided with any 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 upper bounds for the algorithms of Mayr (1981) and Leroux (2011) by extending their approach.