Number-Set Representations for Infinite-State Verification

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.