Automata Modulo Theories

Finite automata are one of the most fundamental models of computation and are taught in almost all undergraduate computer-science curricula. Although automata are typically presented as a theoretical model of computation, they have found their place in a variety of practical applications, such as natural language processing, networking, program verification, and regular-expression matching. In this article, we argue that the classical definition of finite automata is not well suited for practical implementation and present symbolic automata, a model that addresses this limitation.

Back to Top

Key Insights

In most of the literature, finite automata are intuitively presented as follows. A finite automaton is a graph that describes a set of strings over a finite alphabet Σ. In the graph, nodes are called states, some states are initial, some states are final, and each edge "reads" a symbol from Σ. Every path from an initial to a final state describes a string accepted by the automaton. For example, the automaton in Figure 1(a), given Σ = {0, 1}, describes the set of all binary strings starting with 0. Researchers have designed a number of decision procedures and extensions for this simple but very powerful model.