Detail práce
Efektivní knihovna pro práci s konečnými stromovými automaty
Mnoho současných počítačových systémů používá dynamické datové či řídicí struktury předem neomezené velikosti. Tyto datové struktury mají často charakter stromů nebo se dají zakódovat jako stromy s některými dodatečnými ukazateli nad stromovou kostrou. Této skutečnosti využívají některé v současné době intenzivně studované techniky formální verifikace, které reprezentují nekonečně mnoho stavů konečným stromovým automatem. Nicméně v současnosti neexistuje efektivní a flexibilní implementace knihovny pro stromové automaty, která by byla pro tyto techniky vhodná. Cílem této diplomové práce je takovouto knihovnu poskytnout. Předložený text nejdříve popisuje základy teorie konečných stromových automatů a regulárních stromových jazyků. Dále jsou prozkoumány existující implementace knihoven pro stromové automaty a různé verifikační techniky pro systémy se stromovou strukturou. Poté se text zaobírá návrhem reprezentace stromového automatu a algoritmů provádějících standardní jazykové operace nad touto reprezentací, načež následuje popis implementace knihovny. Prostřednictvím provedených experimentů ukazujeme, že knihovna může konkurovat ostatním dostupným knihovnám pro práci se stromovými automaty, přičemž její výkon v určitých oblastech je řádově vyšší.
stromové automaty, formální verifikace, abstraktní regulární stromový model checking, binární rozhodovací diagramy, multiterminálové binární rozhodovací diagramy
Burget Radek, doc. Ing., Ph.D. (UIFS FIT VUT), člen
Janoušek Vladimír, doc. Ing., Ph.D. (UITS FIT VUT), člen
Kotásek Zdeněk, doc. Ing., CSc. (UPSY FIT VUT), člen
Krejčíček Jaromír, prof. Ing., CSc. (UNOB), člen
Švéda Miroslav, prof. Ing., CSc. (UIFS FIT VUT), člen
@mastersthesis{FITMT7985,
author = "Ond\v{r}ej Leng\'{a}l",
type = "Diplomov\'{a} pr\'{a}ce",
title = "Efektivn\'{i} knihovna pro pr\'{a}ci s kone\v{c}n\'{y}mi stromov\'{y}mi automaty",
school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
year = 2010,
location = "Brno, CZ",
language = "czech",
url = "https://www.fit.vut.cz/study/thesis/7985/"
}