Linearizing bad sequences: upper bounds for the product and majoring well quasi-orders

SERGIO ABRIOLA; SANTIAGO FIGUEIRA; GABRIEL SENNO

LECTURE NOTES IN COMPUTER SCIENCE

Springer

Año: 2012 vol. 7456 p. 110 - 126

0302-9743

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 $NN^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 $NN^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 {em linearize} bad sequences, i.e. transform them into a descending one over a well-order for which upper bounds can be more easily handled.