Linearizing well quasi-orders and bounding the length of bad sequences

Abstract

We study the length functions of controlled bad sequences over some well quasi-orders (wqo's) and classify them in the Fast Growing Hierarchy. We develop a new and self-contained study of the length of bad sequences over the disjoint product in Nn (Dickson's Lemma), which leads to recently discovered upper bounds but through a simpler argument. We also give a tight upper bound for the length of controlled decreasing sequences of multisets of Nn with the underlying lexicographic ordering, and use it to give an upper bound for the length of controlled bad sequences in the majoring ordering with the underlying disjoint product ordering. We apply this last result to attain complexity upper bounds for the emptiness problem of itca and atra automata. For the case of the product and majoring wqo's the idea is to linearize bad sequences, i.e. to transform a bad sequence over a wqo into a decreasing one over a well-order, for which upper bounds can be more easily handled.