Ackermannian and Primitive-Recursive Bounds with Dickson's Lemma

Abstract

Dickson's Lemma is a simple yet powerful tool widely used in termination proofs, especially when dealing with counters or related data structures. However, most computer scientists do not know how to derive complexity upper bounds from such termination proofs, and the existing literature is not very helpful in these matters. We propose a new analysis of the length of bad sequences over (N^k,\leq) and explain how one may derive complexity upper bounds from termination proofs. Our upper bounds improve earlier results and are essentially tight.

References in corpus (2)

• Multiply-Recursive Upper Bounds with Higman's Lemma
• On Pebble Automata for Data Languages with Decidable Emptiness Problem

Cited by in corpus (24)

• Demystifying Reachability in Vector Addition Systems
• Complexity Hierarchies Beyond Elementary
• Multiply-Recursive Upper Bounds with Higman's Lemma
• The Power of Well-Structured Systems
• Alternating register automata on finite words and trees
• Non-Elementary Complexities for Branching VASS, MELL, and Extensions
• Affine Extensions of Integer Vector Addition Systems with States
• Complexity Bounds for Ordinal-Based Termination
• Relating timed and register automata
• On bounds for the effective differential Nullstellensatz
• History-Register Automata
• The Containment Problem for Unambiguous Register Automata
• Statures and Sobrification Ranks of Noetherian Spaces
• On the Length of Strongly Monotone Descending Chains over ${\mathbb{N}}^d$
• Decidability and Complexity in Weakening and Contraction Hypersequent Substructural Logics
• Complexity of controlled bad sequences over finite sets of ${\mathbb{N}}^d$
• Path Checking for MTL and TPTL over Data Words
• Reverse Mathematical Bounds for the Termination Theorem
• Implicational Relevance Logic is 2-EXPTIME-Complete
• Explicit polynomial bounds on prime ideals in polynomial rings over fields
• New Techniques for Universality in Unambiguous Register Automata
• Dickson's lemma and weak Ramsey theory
• The strength of SCT soundness
• Non-dominating sequences of vectors using only resets and increments