Don't Care Words with an Application to the Automata-Based Approach for Real Addition

摘要

Automata are a useful tool in infinite-state model checking, since they can represent infinite sets of integers and reals. However, analogous 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 "don't cares" for BDDs to word languages as a means to reduce the automata sizes. We show that the minimal weak deterministic Buechi 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.