Detail publikace

Regular Model Checking Using Inference of Regular Languages

HABERMEHL, P. VOJNAR, T.

Originální název

Regular Model Checking Using Inference of Regular Languages

Typ

článek v časopise - ostatní, Jost

Jazyk

angličtina

Originální abstrakt

Regular model checking is a method for verifying infinite-state 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 infinite-state systems whose behaviour can be modelled using length-preserving 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.

Klíčová slova

formal verification, model checking, parametric systems, infinite-state systems, automata theory, inference of regular languages

Autoři

HABERMEHL, P.; VOJNAR, T.

Rok RIV

2005

Vydáno

28. 12. 2005

ISSN

1571-0661

Periodikum

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE

Ročník

138

Číslo

3

Stát

Spojené státy americké

Strany od

21

Strany do

36

Strany počet

16

URL

http://www.sciencedirect.com/science?_ob=MImg&_imagekey=B75H1-4HTK6GS-3-1&_cdi=13109&_user=640830&_orig=browse&_coverDate=12%2F28%2F2005&_sk=998619996&view=c&wchp=dGLbVlb-zSkWb&md5=540cbefd35764de82d5aa84e0d778934&ie=/sdarticle.pdf

BibTex

@article{BUT45074,
  author="Peter {Habermehl} and Tomáš {Vojnar}",
  title="Regular Model Checking Using Inference of Regular Languages",
  journal="ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE",
  year="2005",
  volume="138",
  number="3",
  pages="21--36",
  issn="1571-0661",
  url="http://www.sciencedirect.com/science?_ob=MImg&_imagekey=B75H1-4HTK6GS-3-1&_cdi=13109&_user=640830&_orig=browse&_coverDate=12%2F28%2F2005&_sk=998619996&view=c&wchp=dGLbVlb-zSkWb&md5=540cbefd35764de82d5aa84e0d778934&ie=/sdarticle.pdf"
}