Název: Efektivní knihovna pro práci s konečnými stromovými automaty
Překlad názvu: An Efficient Finite Tree Automata Library
Autoři: Lengál, Ondřej ; Konečný, Filip (oponent) ; Vojnar, Tomáš (vedoucí práce)
Typ dokumentu: Diplomové práce
Rok: 2010
Jazyk: cze
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [cze] [eng]
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šší. Numerous computer systems use dynamic control and data structures of unbounded size. These data structures have often the character of trees or they can be encoded as trees with some additional pointers. This is exploited by some currently intensively studied techniques of formal verification that represent an infinite number of states using a finite tree automaton. However, currently there is no tree automata library implementation that would provide an efficient and flexible support for such methods. Thus the aim of this Mas- ter's Thesis is to provide such a library. The present paper first describes the theoretical background of finite tree automata and regular tree languages. Then it surveys the cur- rent implementations of tree automata libraries and studies various verification techniques, outlining requirements for the library. Representation of a finite tree automaton and algo- rithms that perform standard language operations on this representation are proposed in the next part, which is followed by description of library implementation. Through a series of experiments it is shown that the library can compete with other available tree automata libraries, in certain areas being even significantly superior to them.
Klíčová slova: abstraktní regulární stromový model checking; binární rozhodovací diagramy; formální verifikace; multiterminálové binární rozhodovací diagramy; stromové automaty; abstract regular tree model checking; binary decision diagrams; formal verification; multiterminal binary decision diagrams; tree automata

Instituce: Vysoké učení technické v Brně (web)
Informace o dostupnosti dokumentu: Plný text je dostupný v Digitální knihovně VUT.
Původní záznam: http://hdl.handle.net/11012/54375

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-237232


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Vysoké učení technické v Brně
Vysokoškolské kvalifikační práce > Diplomové práce