Reference : Omega-regular model checking
Scientific congresses and symposiums : Paper published in a journal
Engineering, computing & technology : Computer science
Omega-regular model checking
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) >]
Lecture Notes in Computer Science
10th International Conference, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004
March 29 - April 2, 2004
[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).
The original publication is available at

File(s) associated to this reference

Fulltext file(s):

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.