Don't Care Words with an Application to the Automata-Based Approach for Real Addition (Extended Abstract)
Jochen Eisinger, Felix Klaedtke · 2006
Automata are a useful tool in infinite-state model checking, since they can represent infinite sets of integers and reals. However, anal- ogous to the use of bdds to represent finite sets, the sizes of the automata are an obstacle in the automata-based set representation. In this paper, we generalize the notion of for bdds to word languages as a means to reduce the automata sizes. We show that the minimal weak deterministic Buchi automaton (wdba) with respect to a given don't care set, under certain restrictions, is uniquely determined and can be efficiently constructed. We apply don't cares to improve the efficiency of a decision procedure for the first-order logic over the mixed linear arithmetic over the integers and the reals based on wdbas.