Multiply-Recursive Upper Bounds with Higman's Lemma

We develop a new analysis for the length of controlled bad sequences in well-quasi-orderings based on Higman’s Lemma. This leads to tight multiply-recursive upper bounds that readily apply to several verification algorithms for well-structured systems. Keywords. Higman’s Lemma; Well-structured systems; Verification; Complexity of algorithms.

• Type: Journal
• Year: 2011
• Where: CORR
• Authors: Sylvain Schmitz, Philippe Schnoebelen
• Keywords: Algorithms, CORR 2011, Education, Multiply-recursive Upper Bounds, Well-structured Systems