Conference paperHABERMEHL Peter and VOJNAR Tomáš. Regular Model Checking Using Inference of Regular Languages. In: Proceedings of 6th International Workshop on Verification of InfiniteState Systems  INFINITY 2004. London, 2004, pp. 6171.  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:  6171 

Proceedings:  Proceedings of 6th International Workshop on Verification of InfiniteState Systems  INFINITY 2004 

Conference:  6th International Workshop on Verification of InfiniteState Systems  INFINITY 2004, a satellite workshop of 15th International Conference on Concurrency Theory  CONCUR 2004 

Place:  London, GB 

Year:  2004 

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: 

@INPROCEEDINGS{
author = {Peter Habermehl and Tom{\'{a}}{\v{s}} Vojnar},
title = {Regular Model Checking Using Inference of Regular Languages},
pages = {6171},
booktitle = {Proceedings of 6th International Workshop on Verification of
InfiniteState Systems  INFINITY 2004},
year = {2004},
location = {London, GB},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php?id=7616}
} 
