Comparison of LTL to Deterministic Rabin Automata Translators

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
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

Citace
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:

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