Article (Scientific journals)
On (Omega-)regular model checking
Legay, Axel; Wolper, Pierre
2010In ACM Transactions on Computational Logic, 12 (1), p. 46
Peer Reviewed verified by ORBi
 

Files


Full Text
paper.pdf
Author postprint (697.62 kB)
Download

© ACM, 2010. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM Transactions on Computational Logic, Vol 12, Number 1, October 2010 http://dx.doi.org/10.1145/1838552.1838554


All documents in ORBi are protected by a user license.

Send to



Details



Keywords :
verification; model-checking; automata
Abstract :
[en] Checking infinite-state systems is frequently done by encoding infinite sets of states as regular languages. Computing such a regular representation of, say, the set of reachable states of a system requires acceleration techniques that can finitely compute the effect of an unbounded number of transitions. Among the acceleration techniques that have been proposed, one finds both specific and generic techniques. Specific techniques exploit the particular type of system being analyzed, for example, a system manipulating queues or integers, whereas generic techniques only assume that the transition relation is represented by a finite-state transducer, which has to be iterated. In this article, we investigate the possibility of using generic techniques in cases where only specific techniques have been exploited so far. Finding that existing generic techniques are often not applicable in cases easily handled by specific techniques, we have developed a new approach to iterating transducers. This new approach builds on earlier work, but exploits a number of new conceptual and algorithmic ideas, often induced with the help of experiments, that give it a broad scope, as well as good performances.
Disciplines :
Computer science
Author, co-author :
Legay, Axel ;  Université de Liège - ULiège > Département d'Electricité, Electronique et Informatique
Wolper, Pierre  ;  Université de Liège - ULiège > Département d'Electricité, Electronique et Informatique
Language :
English
Title :
On (Omega-)regular model checking
Publication date :
2010
Journal title :
ACM Transactions on Computational Logic
ISSN :
1529-3785
Publisher :
Association for Computing Machinery, New-York, United States - New York
Volume :
12
Issue :
1
Pages :
46 p.
Peer reviewed :
Peer Reviewed verified by ORBi
Available on ORBi :
since 12 January 2011

Statistics


Number of views
96 (17 by ULiège)
Number of downloads
186 (7 by ULiège)

Scopus citations®
 
1
Scopus citations®
without self-citations
0
OpenCitations
 
2

Bibliography


Similar publications



Contact ORBi