ORBi: Boigelot Bernard - The Power of QDDs

Reference : The Power of QDDs


	Document type :	Scientific congresses and symposiums : Paper published in a journal
	Discipline(s) :	Engineering, computing & technology : Computer science
	To cite this reference:	http://hdl.handle.net/2268/74879

Title :	The Power of QDDs
Language :	English
Author, co-author :	Boigelot, Bernard [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 [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique > >]
Publication date :	1997
Journal title :	Lecture Notes in Computer Science
Publisher :	Springer
Volume :	1302
Pages :	172-186
On invitation :	No
Audience :	International
ISSN :	0302-9743
e-ISSN :	1611-3349
City :	Berlin
Country :	Germany
Event name :	Static Analysis, 4th International Symposium (SAS '97)
Event place (city) :	Paris
Event country :	France
Keywords :	[en] symbolic state-space exploration ; FIFO channels ; QDDs
Abstract :	[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.
Funders :	Fonds de la Recherche Scientifique (Communauté française de Belgique) - F.R.S.-FNRS, Bell Laboratories
Target :	Researchers
Permalink :	http://hdl.handle.net/2268/74879
Mentions required by the publisher for OA :	The original publication is available at www.springerlink.com

File(s) associated to this reference

Fulltext file(s):

	File	Commentary	Version	Size	Access
Open access	BGWW97.pdf		Author preprint	194.34 kB	View/Open

All documents in ORBi are protected by a user license.

Dspace v1.5