Simplification of finite automata (ENS Project Proposal)

Scope Nondeterministic finite automata (NFA) [7] can be seen as a data structure to represent a (possibly infinite) set of words. In this view, they can be seen as a basic component used in solving problems in different domains, e.g., decision procedures for logical theories (c.f. the MONA tool [4, 5]), program analysis [6], model checking [10], and various reachability problems. NFAs enjoy closure under boolean operations, but while union and intersection are relatively cheap to perform, complementation is exponential in the worst case. Classic decision problems on NFA are emptiness, universality, inclusion, and equivalence; however, they do not have the same complexity, and while emptiness LOGSPACE-complete, the others are already PSPACE-complete. Since procedures manipulating and testing automata might perform many boolean operations on them and expensive tests, it is of crucial importance to keep the size of intermediate automata as small as possible.