Ackermannian and Primitive-Recursive Bounds with Dickson's Lemma

2010/07/31 by Diego Figueira, Santiago Figueira, Sylvain Schmitz +1 · 2 citations
Computer Science · #cs.LO #cs.CC

paper · pdf · doi:10.1109/lics.2011.39

published as In LICS 2011, 26th Annual IEEE Symposium on Logic in Computer Science, pages 269--278. IEEE Press

arxiv created 2011/07/19 · arxiv updated 2011/07/20

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,≤) and explain how one may derive complexity upper bounds from termination proofs. Our upper bounds improve earlier results and are essentially tight.

Cited by

• Reachability in VASS Extended with Integer Counters
• The Complexity of Nested Reset Counter Systems

Related

• Multiply-Recursive Upper Bounds with Higman's Lemma
• Complexity Bounds for Ordinal-Based Termination
• Complexity of controlled bad sequences over finite sets of ℕ^d
• An Application of Markov Chain Analysis to Integer Complexity
• Positive Almost-Sure Termination -- Complexity and Proof Rules