Všechny publikace
| 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}
} |
|