zbMATH — the first resource for mathematics

Linearizing bad sequences: upper bounds for the product and majoring well quasi-orders. (English) Zbl 1361.68102
Ong, Luke (ed.) et al., Logic, language, information and computation. 19th international workshop, WoLLIC 2012, Buenos Aires, Argentina, September 3–6, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32620-2/pbk). Lecture Notes in Computer Science 7456, 110-126 (2012).
Summary: Well quasi-orders (wqo’s) are an important mathematical tool for proving termination of many algorithms. Under some assumptions upper bounds for the computational complexity of such algorithms can be extracted by analyzing the length of controlled bad sequences.
We develop a new, self-contained study of the length of bad sequences over the product ordering of \(\mathbb N^{n }\), which leads to known results but with a much simpler argument.
We also give a new tight upper bound for the length of the longest controlled descending sequence of multisets of \(\mathbb N^{n }\), and use it to give an upper bound for the length of controlled bad sequences in the majoring ordering of sets of tuples. We apply this upper bound to obtain complexity upper bounds for decision procedures of automata over data trees.
In both cases the idea is to linearize bad sequences, i.e. transform them into a descending one over a well-order for which upper bounds can be more easily handled.
For the entire collection see [Zbl 1246.03015].
68Q25 Analysis of algorithms and problem complexity
03D20 Recursive functions and relations, subrecursive hierarchies
03E05 Other combinatorial set theory
68Q45 Formal languages and automata
Full Text: DOI