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

BLAHOUDEK, František, Tomáš BABIAK, Mojmír KŘETÍNSKÝ a Jan STREJČEK. Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment. In Hung Dang-Van and Mizuhito Ogawa. 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013. Berlin Heidelberg: Springer. s. 24-38. ISBN 978-3-319-02443-1. doi:10.1007/978-3-319-02444-8_4. 2013.

Základní údaje

• Originální název: 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 (203 Česká republika, domácí), Tomáš BABIAK (703 Slovensko, domácí), Mojmír KŘETÍNSKÝ (203 Česká republika, domácí) a Jan STREJČEK (203 Česká republika, garant, domácí).
• Vydání: Berlin Heidelberg, 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013, od s. 24-38, 15 s. 2013.
• Nakladatel: Springer

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Stať ve sborníku
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Spojené státy
• Utajení: není předmětem státního či obchodního tajemství
• Forma vydání: tištěná verze "print"
• Impakt faktor: Impact factor: 0.402 v roce 2005
• Kód RIV: RIV/00216224:14330/13:00066175
• Organizační jednotka: Fakulta informatiky
• ISBN: 978-3-319-02443-1
• ISSN: 0302-9743
• Doi: http://dx.doi.org/10.1007/978-3-319-02444-8_4
• Klíčová slova anglicky: linear temporal logic; deterministic omega-automata
• Štítky: best, core_A, firank_A, formela-conference, inear time logic, LTL, translation to deterministic Rabin automata
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

Some applications of linear temporal logic (LTL) require to translate formulae of the logic to deterministic omega-automata. There are currently two translators producing deterministic automata: ltl2dstar working for the whole LTL and Rabinizer applicable to the fragment LTL(F,G). We present a new translation to deterministic Rabin automata via alternating automata and deterministic transition-based generalized Rabin automata. Our translation applies to a fragment that is strictly larger than LTL(F,G). Experimental results show that our algorithm can produce significantly smaller automata compared to Rabinizer and ltl2dstar, especially for more complex LTL formulae.

Anotace česky

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.

Návaznosti

• GBP202/12/G061, projekt VaV: Název: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Akronym: CE-ITI)

Investor: Grantová agentura ČR, Centrum excelence - Institut teoretické informatiky

• MUNI/A/0739/2012, interní kód MU: Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

• MUNI/A/0760/2012, interní kód MU: Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II. (Akronym: FI MAV II.)

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty