In order to compute the reachability set of infinite-state models, one needs a technique for exploring infinite sequences of transitions in finite time, as well as a symbolic representation for the finite and infinite sets of configurations that are to be handled. The representation problem can be solved by automata-based methods, which consist in representing a set by a finite-state machine recognizing its elements, suitably encoded as words over a finite alphabet. Automata-based set representations have many advantages: They are expressive, easy to manipulate, and admit a canonical form.
In this survey, we describe two automata-based structures that have been developed for representing sets of numbers (or, more generally, of vectors): The Number Decision Diagram (NDD) for integer values, and the Real Vector Automaton (RVA) for real numbers. We discuss the expressiveness of these structures, present some construction algorithms, and give a brief introduction to some related acceleration techniques.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com