Thesis Details
Model checking nekonečně stavových systémů založený na inferenci jazyků
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 implement regular model checking using inference of regular languages. The method builds upon the observations that for infinite-state systems whose behavior can be modeled using length-preserving transducers, there is a finite computation for obtaining all reachable configurations. Our new approach to regular model checking via inference of regular languages is based on the Angluin's L* algorithm that is used for finding out an invariant which can answer our question whether the system satisfies some property. We also provide an intro to the theory of finite automata, model checking, SAT solving and Anguin's L* and Bierman algorithm of learning finite automata.
Finite automate, Angluin's L* algorithm, Bierman algorithm, model checking, regular model checking, formal verification
Ryšavý Ondřej, doc. Ing., Ph.D. (DIFS FIT BUT), člen
Sumec Stanislav, Ing., Ph.D. (DCGM FIT BUT), člen
Šafařík Jiří, prof. Ing., CSc. (WBU in Pilsen), člen
Zbořil František, doc. Ing., Ph.D. (DITS FIT BUT), člen
Zendulka Jaroslav, doc. Ing., CSc. (DIFS FIT BUT), člen
@mastersthesis{FITMT5967,
author = "Pavel Rozehnal",
type = "Master's thesis",
title = "Model checking nekone\v{c}n\v{e} stavov\'{y}ch syst\'{e}m\r{u} zalo\v{z}en\'{y} na inferenci jazyk\r{u}",
school = "Brno University of Technology, Faculty of Information Technology",
year = 2007,
location = "Brno, CZ",
language = "czech",
url = "https://www.fit.vut.cz/study/thesis/5967/"
}