Reference : Number-Set Representations for Infinite-State Verification
Scientific congresses and symposiums : Paper published in a book
Engineering, computing & technology : Computer science
Number-Set Representations for Infinite-State Verification
Boigelot, Bernard mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique >]
Proceedings of VISSAS 2005
IOS Press
NATO Security through Science Series D: Information and Communication Security
NATO Advanced Research Workshop "Verification of Infinite State Systems with Applications to Security (VISSAS 2005)"
March 2005
[en] Infinite-state systems ; symbolic representations ; number-set representations
[en] 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.

File(s) associated to this reference

Fulltext file(s):

Open access
B05.pdfAuthor preprint239.36 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.