Reference : Omega-regular model checking
Scientific congresses and symposiums : Paper published in a journal
Engineering, computing & technology : Computer science
http://hdl.handle.net/2268/18666
Omega-regular model checking
English
Boigelot, Bernard mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique >]
Legay, A. [Université de Liège - ULG > Depart. d'électricité, électronique et informatique (Institut Montefiore) > informatique > >]
Wolper, Pierre mailto [Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique (parallélisme et banques de données) >]
2004
Lecture Notes in Computer Science
Springer
2988
LECTURE NOTES IN COMPUTER SCIENCE
561-575
Yes
International
0302-9743
1611-3349
Berlin
Germany
10th International Conference, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004
March 29 - April 2, 2004
Barcelona
Spain
[en] model checking ; infinite state
[en] "Regular model checking" is the name of a family of techniques for analyzing infinite-state systems in which states are represented by words or trees, sets of states by finite automata on these objects, and transitions by finite automata operating on pairs of state encodings, i.e. finite-state transducers. In this context, the central problem is then to compute the iterative closure of a finite-state transducer. This paper addresses the use of regular model-checking like techniques for systems whose states are represented by infinite (omega) words. Its main motivation is to show the feasibility and usefulness of this approach through a combination of the necessary theoretical developments, implementation, and experimentation. The iteration technique that is used is adapted from recent work of the authors on the iteration of finite-word transducers. It proceeds by comparing successive elements of a sequence of approximations of the iteration, detecting an "increment" that is added to move from one approximation to the next, and extrapolating the sequence by allowing arbitrary repetitions of this increment. By restricting oneself to weak deterministic Buchi automata, and using a number of implementation optimizations, examples of significant size can be handled. The proposed transducer iteration technique can just as well be exploited to compute the closure of a given set of states by the transducer iteration, which has proven to be a very effective way of using the technique. Examples such as a leaking gas burner in which time is modeled by real variables have been handled completely within the automata-theoretic setting.
Communauté française de Belgique - Direction de la recherche scientifique - Actions de recherche concertées ; European IST-FET project ADVANCE (IST-1999-29082).
Researchers
http://hdl.handle.net/2268/18666
The original publication is available at www.springerlink.com

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
BLW04-tacas.pdfAuthor postprint178.16 kBView/Open
Restricted access
BLW04-TACAS.pdfPublisher postprint208.07 kBRequest copy

Bookmark and Share SFX Query

All documents in ORBi are protected by a user license.