Don't care words with an application to the automata-based approach for real addition
Seminar Room 1, Newton Institute
As already pointed out by Buechi, automata can be used to decide certain first-order theories of linear arithmetic, like the first-order theory over the reals with addition and the ordering. Reals are represented as omega-words (e.g., using the 2's complement representation), and the automata are recursively constructed from the formulas. The constructed automaton for a formula precisely accepts the words representing the reals that make the formula true. This automata-based approach for representing and manipulating sets of reals has also applications in infinite state model checking. However, analogous to BDDs to represent finite sets, the sizes of the automata are an obstacle in the automata-based set representation.
In this talk, I will show that so-called "don't cares sets" for BDDs can be generalized to word languages as a means to reduce the automata sizes and how "don't care words" can be used to build a more effective automata-based decision procedure for real addition. A general result about don't care words is that the minimal weak deterministic Buechi automaton with respect to a given don't care set with certain restrictions is uniquely determined and can be constructed efficiently.