Reference : Verifying Systems with Infinite but Regular State Spaces
Scientific congresses and symposiums : Paper published in a journal
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/74875
Verifying Systems with Infinite but Regular State Spaces
English
Wolper, Pierre mailto [Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique > >]
Boigelot, Bernard mailto [Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique >]
1998
Lecture Notes in Computer Science
Springer
1427
88-97
No
Yes
International
0302-9743
1611-3349
Berlin
Germany
Computer Aided Verification, 10th International Conference (CAV 1998)
Vancouver
Canada
[en] verification ; infinite state spaces ; symbolic representations
[en] Thanks to the development of a number of efficiency enhancing
techniques, state-space exploration based verification, and in
particular model checking, has been quite successful for finite-state
systems. This has prompted efforts to apply a similar approach to
systems with infinite state spaces. Doing so amounts to developing
algorithms for computing a symbolic representation of the infinite
state space, as opposed to requiring the user to characterize the
state space by assertions. Of course, in most cases, this can only be
done at the cost of forgoing any general guarantee of success. The
goal of this paper is to survey a number of results in this area and
to show that a surprisingly common characteristic of the systems that
can be analyzed with this approach is that their state space
can be represented as a regular language.
Fonds de la Recherche Scientifique (Communauté française de Belgique) - F.R.S.-FNRS
Researchers
http://hdl.handle.net/2268/74875
10.1007/BFb0028736
The original publication is available at www.springerlink.com

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
WB98.pdfAuthor preprint263.53 kBView/Open

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.