Comparison of LTL to Deterministic Rabin Automata Translators

• Název česky: Srovnání překladačů LTL na deterministické Rabinovy automaty
• Autoři: BLAHOUDEK František; KŘETÍNSKÝ Mojmír; STREJČEK Jan
• Rok publikování: 2013
• Druh: Článek ve sborníku
• Konference: Logic for Programming Artificial Intelligence and Reasoning, LPAR-19
• Fakulta / Pracoviště MU: Fakulta informatiky
• Doi: http://dx.doi.org/10.1007/978-3-642-45221-5_12
• Obor: Informatika
• Klíčová slova: linear temporal logic; deterministic omega-automata; LTL3DRA; Rabinizer; ltl2dstar
• Popis: Narůstající zájem o syntézu a pravděpodobnostní model checking pohání pokrok v oblasti překladu LTL na deterministické omega-automaty. Typický překlad, implementovaný v nástroji ltl2dstar, využívá Safrovu konstrukci ke zdeterminizování Büchiho automatu, jež vzniknul pomocí libovolného překladače LTL na Büchiho automaty. Od roku 2012 byly uvedeny tři nové překladače LTL na deterministické Rabinovy automaty. Jmenovitě Rabinizer, LTL3DRA a Rabinizer 2. Všechny pracují pouze pro fragmenty LTL, na druhou stranu nepoužívají Safrovu konstrukci. V naší práci porovnáváme rychlost a výsledné automaty uvedených nástrojů, přičemž ltl2dstar je kombinováno s několika překladači LTL na Büchiho automaty: kromě tradičního LTL2BA také LTL->NBA, LTL3BA a Spot.

Související projekty

• Formální metody pro analýzu a verifikaci komplexních systémů
• Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity
• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace II.