Journal articleHABERMEHL Peter and VOJNAR Tomáš. Regular Model Checking Using Inference of Regular Languages. Electronic Notes in Theoretical Computer Science. 2005, vol. 138, no. 3, pp. 2136. ISSN 15710661.  Publication language:  english 

Original title:  Regular Model Checking Using Inference of Regular Languages 

Title (cs):  Regulární model checking založený na učení jazyků 

Pages:  2136 

Book:  Proceedings of the 6th International Workshop on Verification of InfiniteState Systems (INFINITY 2004) 

Year:  2005 

Journal:  Electronic Notes in Theoretical Computer Science, Vol. 138, No. 3, US 

ISSN:  15710661 

URL:  http://www.sciencedirect.com/science?_ob=MImg&_imagekey=B75H14HTK6GS31&_cdi=13109&_user=640830&_orig=browse&_coverDate=12%2F28%2F2005&_sk=998619996&view=c&wchp=dGLbVlbzSkWb&md5=540cbefd35764de82d5aa84e0d778934&ie=/sdarticle.pdf [PDF] 

Keywords 

formal verification, model checking, parametric systems, infinitestate systems, automata theory, inference of regular languages 
Annotation 

Regular model checking is a method for verifying infinitestate systems
based on coding their configurations as words over a finite alphabet,
sets of configurations as finite automata, and transitions as finite
transducers. We introduce a new general approach to regular model
checking based on inference of regular languages. The method builds
upon the observation that for infinitestate systems whose behaviour
can be modelled using lengthpreserving transducers, there is a
finite computation for obtaining all reachable configurations up
to a certain length n.
These configurations are a (positive) sample of the reachable
configurations of the given system, whereas~all other words up to
length n are a negative sample. Then, methods of inference of regular
languages can be used to generalise the sample to the full reachability
set (or an overapproximation of it). We have implemented our method in
a prototype tool which shows that our approach is competitive on a
number of concrete examples. Furthermore, in contrast to all other
existing regular model checking methods, termination is guaranteed in
general for all systems with regular sets of reachable configurations.
The method can be applied in a similar way to dealing with reachability
relations instead of reachability sets too. 
BibTeX: 

@ARTICLE{
author = {Peter Habermehl and Tom{\'{a}}{\v{s}} Vojnar},
title = {Regular Model Checking Using Inference of Regular
Languages},
pages = {2136},
booktitle = {Proceedings of the 6th International Workshop on
Verification of InfiniteState Systems (INFINITY 2004)},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {138},
number = {3},
year = {2005},
ISSN = {15710661},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php?id=7999}
} 
