Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment

Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Název česky Efektivní překlad LTL na deterministické Rabinovy automaty
Autoři

BLAHOUDEK František BABIAK Tomáš KŘETÍNSKÝ Mojmír STREJČEK Jan

Rok publikování 2013
Druh Článek ve sborníku
Konference 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-319-02444-8_4
Obor Informatika
Klíčová slova linear temporal logic; deterministic omega-automata
Popis Některé aplikace Lineární temporální logiky (LTL) vyžadují překlad formulí této logiky na deterministické omega-automaty. V současnosti existují dva překladače produkující deterministické automaty: ltl2dstar zpracovávající celou logiku LTL a Rabinizer použitelný pouze na fragmentu LTL (F,G). Představujeme nový algoritmus pro překlad LTL formulí na deterministické Rabinovy automaty přes alternující automaty a deterministické zobecněné Rabinovy automaty s akceptující podmínkou na hranách. Náš překlad funguje pro fragment LTL, který je striktně větší než LTL(F,G). Experimentální výsledky ukazují, že náš algoritmus může produkovat podstatně menší automaty v porovnání s Rabinizerem s ltl2dstar, zejména pro složitější LTL formule.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.