SCS Undergraduate Thesis Topics
|Dan Kilgallin||Klaus Sutner||Complementing Buchi Automata Over Bi-infinite Words|
In this work, we introduce an algorithm that, when given an ω-Bu¨chi automaton (an automaton recognizing languages over one-way infinite words) as input, finds a small automaton that recognizes the complement of the language of that automaton. This procedure is necessary in many tasks, and the current algorithms construct automata much larger than the original. We modify the definition of an ω-Bu¨chi automaton to allow a smaller machine to represent the same language, allowing the complement automata to be smaller as well. We then show that a natural generalization of an existing algorithm for complementing ω-Bu¨chi automata will find the complement of the language of one of these reduced automata. The modification we make to the definition of an automaton is to allow transitions to be labeled with arbitrarily long strings of input characters, rather than restricting them to reading one character at a time. This causes some of the states to become extraneous, which allows us to remove them without changing the language accepted by the automaton. We can iteratively find and remove extraneous nodes, and add transitions between the removed node's neighbors. We explore different possibilities for the ordering in which to remove the nodes that produces the smallest resulting automaton, though the problem in general is NP-complete. This modified version does have some drawbacks, but in some applications of this algorithm, none of these drawbacks are relevant. We focus on one such application - deciding properties of cellular automata that can be described with a formula of first-order logic containing a single universal quantifier. These properties can be verified with operations on a ξ-Bu¨chi automaton (an automaton recognizing languages over bi-infinite words) on a de Bruijn graph, but the presence of a universal quantifier requires taking the complement of the language, causing a superexponential blowup in the number of states required. We show that by converting the ξ-Bu¨chi automaton to a reduced ω-Bu¨chi before performing this step, we can greatly reduce the number of states in the complement automaton.