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. 
Sylvain Schmitz and Philippe Schnoebelen
cs.LO cs.CC