| Holík, L.: Simulations and Antichains for Efficient Handling of Finite Automata, Brno, CZ, UITS FIT VUT, 2011, s. 128 | | Jazyk publikace: | angličtina |
|---|
| Název publikace: | Simulations and Antichains for Efficient Handling of Finite Automata |
|---|
| Název (cs): | Simulace a protiřetězce pro práci s konečnými automaty |
|---|
| Strany: | 128 |
|---|
| Místo vydání: | Brno, CZ |
|---|
| Rok: | 2011 |
|---|
| Vydavatel: | Ústav inteligentních systémů FIT VUT v Brně |
|---|
| Soubory: | |
|---|
|
| | Klíčová slova |
|---|
Konecný automat, konecný stromový automat, alternující Büchiho automat,
nedeterminismus, univerzalita, jazyková inkluze, protiretezec, simulace, bisimulace,
redukce velikosti, regulární stromový model checking. |
| Abstrakt |
|---|
Cílem této práce je vývoj technik umožnujících praktické využití nedeterministických
konecných automatu, zejména nedeterministických stromových automatu.
Jde zvlášte o techniky pro redukci velikosti a testování jazykové inkluze,
jež hrají zásadní roli v mnoha oblastech aplikace konecných automatu. V oblasti
redukce velikosti vycházíme z dobre známých metod pro slovní automaty které
jsou založeny na relacích simulace. Navrhli jsme efektivní algoritmy pro výpocet
stromových variant simulacních relací a identifikovali jsme nový typ relace založený
na kombinaci takzvaných horních a dolních simulací nad stromovými
automaty. Tyto kombinované relace jsou zvlášte vhodné pro redukci velikosti
automatu slucováním stavu. Navržený princip kombinace relací simulace je relevantní
i pro slovní automaty. Náš prínos v oblasti testování jazykové inkluze
je dvojí. Nejprve jsme zobecnili na stromové automaty takzvané protiretezcové
algoritmy, které byly puvodne navrženy pro slovními automaty. Dále se nám podarilo
použitím simulacních relací výrazne zefektivnit protiretezcové algoritmy
pro testování jazykové inkluze jak pro slovní, tak pro stromové automaty. Relevanci
našich technik pro praxi jsme demonstrovali jejich nasazením v rámci
regulárního stromového model checkingu, což je verifikacní metoda založená
na stromových automatech. Použití našich algoritmu zde vedlo k výraznému
zrychlení a zvetšení škálovatelnosti celé metody. Základní myšlenky našich algoritmu
pro redukci velikosti automatu a testování jazykové inkluze jsou aplikovatelné
i na jiné typy automatu. Príkladem jsou naše redukcní techniky pro
alternující Büchiho automaty prezentované v poslední cásti práce. |
| BibTeX: |
|---|
@PHDTHESIS{
author = {Lukáš Holík},
title = {Simulations and Antichains for Efficient Handling of Finite
Automata},
pages = {128},
year = {2011},
location = {Brno, CZ},
publisher = {Department of Intelligent Systems FIT BUT},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php?id=9517}
} |
|
Fakulta informačních technologií