Multiply-Recursive Upper Bounds with Higman's Lemma

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.

References in corpus (1)

• Ackermannian and Primitive-Recursive Bounds with Dickson's Lemma

Cited by in corpus (15)

• Ackermannian and Primitive-Recursive Bounds with Dickson's Lemma
• Complexity Hierarchies Beyond Elementary
• The Power of Well-Structured Systems
• Graph Logics with Rational Relations
• The Power of Priority Channel Systems
• Complexity Bounds for Ordinal-Based Termination
• The Parametric Ordinal-Recursive Complexity of Post Embedding Problems
• Solving Stochastic Büchi Games on Infinite Arenas with a Finite Attractor
• Generalized Post Embedding Problems
• On Ordinal Invariants in Well Quasi Orders and Finite Antichain Orders
• Well Behaved Transition Systems
• Statures and Sobrification Ranks of Noetherian Spaces
• Decidability and Complexity in Weakening and Contraction Hypersequent Substructural Logics
• Complexity of controlled bad sequences over finite sets of ${\mathbb{N}}^d$
• On the cartesian product of well-orderings