Multiply-Recursive Upper Bounds with Higman's Lemma
arXiv:1103.4399 · doi:10.1007/978-3-642-22012-8_35
Abstract
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.