Original title: Efektivní algoritmy pro stromové automaty
Translated title: Efficient Algorithms for Tree Automata
Authors: Valeš, Ondřej ; Hruška, Martin (referee) ; Lengál, Ondřej (advisor)
Document type: Master’s theses
Year: 2019
Language: cze
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [cze] [eng]
Cílem této práce je navržení efektivních algoritmů pro testování jazykové ekvivalence a inkluze stromových automatů a dále pak implementace těchto algoritmů jako rozšíření knihovny VATA. Nejprve je provedena rešerše existujících přístupů testování ekvivalence a inkluze slovních i stromových automatů. Z nich poté vychází návrh nového přístupu k testování ekvivalence a inkluze jazyků stromových automatů založený na bisimulaci vzhledem ke kongruenci, ke kterému je představen formální důkaz korektnosti. Součástí práce je také srovnání efektivity představeného algoritmu a již existujících přístupů, které ukazuje, že na obtížných případech je náš algoritmus často lepší než existující přístupy. In this work a novel algorithm for testing language equivalence and inclusion on tree automata is proposed and implemented as a module in the VATA library. First, existing approaches to equivalence and inclusion testing on both word and tree automata are examined. These existing approaches are then modified to create bisimulation up-to congruence algorithm for tree automata and a formal proof of the soundness of the new algorithm is provided. Efficiency of this new approach is compared with existing language equivalence and inclusion testing methods for tree automata, showing the performance of our algorithm on hard cases is often superior.
Keywords: antichains; bisimulation; bisimulation up-to congruence; language equivalence; language inclusion; tree automata; word automata; antichainy; bisimulace; bisimulation up-to congruence; jazyková ekvivalence; jazyková inkluze; slovní automaty; stromové automaty

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: http://hdl.handle.net/11012/180360

Permalink: http://www.nusl.cz/ntk/nusl-598532


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Master’s theses