Reference : Symbolic Verification with Periodic Sets
Scientific journals : Article
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/74878
Symbolic Verification with Periodic Sets
English
Boigelot, Bernard mailto [Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique >]
Wolper, Pierre mailto [Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique > >]
1994
Lecture Notes in Computer Science
Springer
818
55-67
Yes
International
0302-9743
1611-3349
Berlin
Germany
[en] symbolic state-space exploration ; infinite-state systems ; verification
[en] Symbolic approaches attack the state explosion problem by introducing
implicit representations that allow the simultaneous manipulation of
large sets of states. The most commonly used representation in this
context is the Binary Decision Diagram (BDD). This paper takes the
point of view that other structures than BDD's can be useful for
representing sets of values, and that combining implicit and explicit
representations can be fruitful. It introduces a representation
of complex periodic sets of integer values, shows how this
representation can be manipulated, and describes its application to the
state-space exploration of protocols. Preliminary experimental results
indicate that the method can dramatically reduce the resources
required for state-space exploration.
Fonds de la Recherche Scientifique (Communauté française de Belgique) - F.R.S.-FNRS. FNRS. This work was supported by the Esprit BRA action REACT and by the Belgian Incentive Program "Information Technology" - Computer Science of the future, initiated by the Belgian State - Prime Minister's Office - Science Policy Office.
Researchers
http://hdl.handle.net/2268/74878
10.1007/3-540-58179-0_43
The original publication is available at www.springerlink.com

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
BW94.pdfAuthor preprint160.55 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.