Reference : Handling Liveness Properties in (ω-)Regular Model Checking
Scientific congresses and symposiums : Paper published in a journal
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/18661
Handling Liveness Properties in (ω-)Regular Model Checking
English
Bouajjani, Ahmed [University of Paris 7, LIAFA]
Legay, Axel [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique > > >]
Wolper, Pierre mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique > >]
28-Dec-2005
Electronic Notes in Theoretical Computer Science
Elsevier
138
3
Proceedings of the 6th International Workshop on Verification of Infinite-State Systems (INFINITY 2004)
101-115
Yes
No
International
1571-0661
1571-0661
Amsterdam
Pays-Bas
6th International Workshop on Verification of Infinite-State Systems
4 septembre 2004
Londres
Angleterre
[en] Regular Model Checking ; Livenss properties
[en] Since the topic emerged several years ago, work on regular model checking has mostly been devoted to the verification of state reachability and safety properties. Though it was known that liveness properties could also be checked within this framework, little has been done about working out the corresponding details, and experimentally evaluating the approach. This paper addresses these issues in the context of regular model checking based on the encoding of states by finite or infinite words. It works out the exact constructions to be used in both cases, and solves the problem resulting from the fact that infinite computations of unbounded configurations might never contain the same configuration twice, thus making cycle detection problematic. Several experiments showing the applicability of the approach were successfully conducted.
Fonds pour la formation à la Recherche dans l'Industrie et dans l'Agriculture (Communauté française de Belgique) - FRIA
Researchers
http://hdl.handle.net/2268/18661
10.1016/j.entcs.2005.02.061
http://www.elsevier.com/wps/find/journaldescription.cws_home/681021/description#description

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
paper-infinity.pdfAuthor postprint230.08 kBView/Open
Restricted access
ALW2005-postprint-editor.pdfPublisher postprint279.11 kBRequest copy

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.