Detail práce

Převod LTL formulí s omezenými operátory do automatů s čítači

Bakalářská práce Student: Slezáková Alexandra Akademický rok: 2019/2020 Vedoucí: Holík Lukáš, doc. Mgr., Ph.D.
Jazyk práce
slovenský
Abstrakt

Táto práca rieši prevod LTL formulí s obmedzenými operátormi (temporálne operátory, ktoré majú obmedzenú platnosť na určitý počet krokov) do automatu s čítačmi. Použitím klasických metód je automatová reprezentácia takýchto formulí veľká, pretože veľkosť automatu môže byť exponenciálna k hornej hranici obmedzenia. Prezentujeme konštrukciu, ktorá vytvára automat nezávislý na obmedzení.

Práca predstavuje riešenie problému pomocou čítačového Büchi automatu. Čítače zaisťujú nevytváranie podobných stavov a prechodov, čo vedie k zmenšeniu veľkosti automatu. Naša metóda je implementovaná a experimentálne overená. Počet stavov automatu pre formule s veľkým obmedzením operátora redukujeme niekoľkonásobne v porovnaní s klasickými metódami.

Klíčová slova

preklad LTL formulí, LTL formule s obmedzenými operátormi, čítačový Büchi automat, lineárna temporálna logika, overovanie modelov

Ústav
Ústav inteligentních systémů FIT VUT v Brně
Studijní program
Informační technologie
Soubory
Stav
obhájeno, hodnocení A
Obhajoba
9. července 2020
Oponent
Smrčka Aleš, Ing., Ph.D.
Průběh obhajoby

Studentka nejprve prezentovala výsledky, kterých dosáhla v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Studentka následně odpověděla na otázky oponenta a na další otázky přítomných. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studentky na položené otázky rozhodla práci hodnotit stupněm A.

Otázky u obhajoby
  1. Jakým způsobem jste měřila výkonnostní parametry u experimentů? Jedná se o jedno spuštění nebo agregaci více běhů?
  2. Podporují ostatní nástroje čítačové automaty? Jak si vede vaše řešení v porovnání s ostatními?
Komise
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT), předseda
Burgetová Ivana, Ing., Ph.D. (UIFS FIT VUT), člen
Grézl František, Ing., Ph.D. (UPGM FIT VUT), člen
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT), člen
Vašíček Zdeněk, doc. Ing., Ph.D. (UPSY FIT VUT), člen
Citace
SLEZÁKOVÁ, Alexandra. Převod LTL formulí s omezenými operátory do automatů s čítači. Brno, 2020. Bakalářská práce. Vysoké učení technické v Brně, Fakulta informačních technologií. 2020-07-09. Vedoucí práce Holík Lukáš. Dostupné z: https://www.fit.vut.cz/study/thesis/22336/
BibTeX 
@bachelorsthesis{FITBT22336,
    author = "Alexandra Slez\'{a}kov\'{a}",
    type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce",
    title = "P\v{r}evod LTL formul\'{i} s omezen\'{y}mi oper\'{a}tory do automat\r{u} s \v{c}\'{i}ta\v{c}i",
    school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
    year = 2020,
    location = "Brno, CZ",
    language = "slovak",
    url = "https://www.fit.vut.cz/study/thesis/22336/"
}

Závěrečné práce

Nahoru