Linearizing bad sequences: Upper bounds for the product and majoring well quasi-orders
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...
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | SER |
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/20.500.12110/paper_03029743_v7456LNCS_n_p110_Abriola |
| Aporte de: |
| Sumario: | 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 ℕ 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 ℕ 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. © 2012 Springer-Verlag. |
|---|