Detail publikačního výsledku

Regular Model Checking Using Inference of Regular Languages

HABERMEHL, P.; VOJNAR, T.

Originální název

Regular Model Checking Using Inference of Regular Languages

Anglický název

Regular Model Checking Using Inference of Regular Languages

Druh

Článek recenzovaný mimo WoS a Scopus

Originální abstrakt

Regular model checking is a method for verifying infinite-state systemsbased on coding their configurations as words over a finite alphabet,sets of configurations as finite automata, and transitions as finitetransducers. We introduce a new general approach to regular modelchecking based on inference of regular languages. The method buildsupon the observation that for infinite-state systems whose behaviourcan be modelled using length-preserving transducers,  there is afinite computation for obtaining all reachable  configurations upto a certain length n.
These configurations are a (positive) sample of the reachableconfigurations of the given system, whereas~all other words up tolength n are a negative sample. Then, methods of inference of regularlanguages can be used to generalise the sample to the full reachabilityset (or an overapproximation of it). We have implemented our method ina prototype tool which shows that our approach is competitive on anumber of concrete examples. Furthermore, in contrast to all otherexisting regular model checking methods, termination is guaranteed ingeneral for all systems with regular sets of reachable configurations.The method can be applied in a similar way to dealing with reachabilityrelations instead of reachability sets too.

Anglický abstrakt

Regular model checking is a method for verifying infinite-state systemsbased on coding their configurations as words over a finite alphabet,sets of configurations as finite automata, and transitions as finitetransducers. We introduce a new general approach to regular modelchecking based on inference of regular languages. The method buildsupon the observation that for infinite-state systems whose behaviourcan be modelled using length-preserving transducers,  there is afinite computation for obtaining all reachable  configurations upto a certain length n.
These configurations are a (positive) sample of the reachableconfigurations of the given system, whereas~all other words up tolength n are a negative sample. Then, methods of inference of regularlanguages can be used to generalise the sample to the full reachabilityset (or an overapproximation of it). We have implemented our method ina prototype tool which shows that our approach is competitive on anumber of concrete examples. Furthermore, in contrast to all otherexisting regular model checking methods, termination is guaranteed ingeneral for all systems with regular sets of reachable configurations.The method can be applied in a similar way to dealing with reachabilityrelations instead of reachability sets too.

Klíčová slova

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

Klíčová slova v angličtině

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

Autoři

HABERMEHL, P.; VOJNAR, T.

Vydáno

28.12.2005

Kniha

Proceedings of the 6th International Workshop on Verification of Infinite-State Systems (INFINITY 2004)

ISSN

1571-0661

Periodikum

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE

Svazek

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"
}