Automata have proved to be a useful tool in infinite-state model checking, since they can represent infinite sets of integers
and reals. However, analogous to the use of binary decision diagrams (
bdds) to represent finite sets, the sizes of the automata are an obstacle in the automata-based set representation. In this article,
we generalize the notion of “don’t cares” for
bdds to word languages as a means to reduce the automata sizes. We show that the minimal weak deterministic Büchi 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.
Keywords Decision procedure - Mixed linear arithmetic over the integers and reals - Automata theory - Verification of infinite-state systems