Multiply-Recursive Upper Bounds with Higman's Lemma

TL;DR

This paper introduces a new analysis method for the length of controlled bad sequences in well-quasi-orderings, resulting in tight multiply-recursive upper bounds applicable to verification algorithms for well-structured systems.

Contribution

It presents a novel analysis based on Higman's Lemma that improves upper bounds for controlled bad sequences in well-quasi-orderings.

Findings

Derived tight multiply-recursive upper bounds

Applicable to verification algorithms for well-structured systems

Enhanced understanding of sequence length limits in well-quasi-orderings

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.