Reference : The Power of QDDs
Scientific congresses and symposiums : Paper published in a journal
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/74879
The Power of QDDs
English
Boigelot, Bernard mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique >]
Godefroid, Patrice [Lucent Technologies > Bell Laboratories > > >]
Willems, Bernard [Université de Liège - ULg > Dept d'électricité, électronique et informatique > > >]
Wolper, Pierre mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique > >]
1997
Lecture Notes in Computer Science
Springer
1302
172-186
Yes
No
International
0302-9743
1611-3349
Berlin
Germany
Static Analysis, 4th International Symposium (SAS '97)
Paris
France
[en] symbolic state-space exploration ; FIFO channels ; QDDs
[en] Queue-content Decision Diagrams (QDDs) are finite-automaton based
data structures for representing (possibly infinite) sets of contents
of a finite collection of unbounded FIFO queues. Their intended use is
to serve as a symbolic representation of the possible queue contents
that can occur in the state space of a protocol modeled by
finite-state machines communicating through unbounded queues. This is
done with the help of a loop-first search, a state-space exploration
technique that attempts whenever possible to compute symbolically the
effect of repeatedly executing a loop any number of times, making it
possible to analyze protocols with infinite state spaces though
without the guarantee of termination. This paper first solves a key
problem concerning the use of QDDs in this context: it precisely
characterizes when, and shows how, the operations required by a
loop-first search can be applied to QDDs. Then, it addresses the
problem of exploiting QDDs and loop-first searches to broaden the
range of properties that can be checked from simple state reachability
to temporal logic. Finally, a sufficient criterion for the
termination of a loop-first search using QDDs is given.
Fonds de la Recherche Scientifique (Communauté française de Belgique) - F.R.S.-FNRS, Bell Laboratories
Researchers
http://hdl.handle.net/2268/74879
The original publication is available at www.springerlink.com

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
BGWW97.pdfAuthor preprint194.34 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.