Mia Minnes
Mia Minnes

Ph.D. (2008) Cornell University

First Position
Dissertation
Advisor:
Research Area:
Abstract: Finite state automata are Turing machines with fixed finite bounds on resource use. Automata lend themselves well to realtime computations and efficient algorithms. Continuing a tradition of studying computability in mathematics, we examine automatic structures, mathematical objects which can be represented by automata, and apply resulting observations to computer science.
We measure the complexity of automatic structures via wellestablished concepts from model theory, topology, and set theory. We prove the following results. The ordinal height of any automatic wellfounded partial order is bounded by ω^{ω}. The ordinal heights of automatic wellfounded relations are unbounded below ω_{1}^{CK}, the first uncomputable ordinal. For any computable ordinal α, there is an automatic structure of Scott rank at least α. Moreover, there are automatic structures of Scott rank ω_{1}^{CK}, ω_{1}^{CK} + 1. For any computable ordinal α, there is an automatic successor tree of CantorBendixson rank α.
Next, we study infinite graphs produced from a natural unfolding operation applied to finite graphs. Graphs produced via such operations have finite degree and can be described by finite automata over a oneletter alphabet. We investigate algorithmic properties of such graphs in terms of their finite presentations. In particular, we ask how hard it is to check whether a given node belongs to an infinite component, whether two given nodes in the graph are reachable from one another, and whether the graph is connected. We give polynomialtime algorithms answering each of these questions. For a fixed input graph, the algorithm for infinite component membership works in constant time and reachability is decided uniformly by a single automaton. Hence, we improve on previous work, in which nonelementary or nonuniform algorithms were found.
We turn our attention to automata techniques for deciding firstorder logical theories. These techniques are useful in Integer Linear Programming and Mixed Integer Linear Programming, which in turn have applications in diverse areas of computer science and engineering. We extend known work to address the enumeration problem for linear programming solutions. Then, we apply a similar paradigm to give an automata theoretic decision procedure for the padic valued ring under addition and for formal Laurent series over a finite field with valuation and addition.