Multiply-Recursive Upper Bounds with Higman's Lemma
Logic in Computer Science
2011-07-20 v2 Computational Complexity
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.
Cite
@article{arxiv.1103.4399,
title = {Multiply-Recursive Upper Bounds with Higman's Lemma},
author = {Sylvain Schmitz and Philippe Schnoebelen},
journal= {arXiv preprint arXiv:1103.4399},
year = {2011}
}