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

• 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
• 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

• Centrum excelence - Institut teoretické informatiky
• Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity
• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II.