Skoro lineární Büchiho automaty

Základní údaje

Originální název Almost linear Büchi automata
Autoři

Další údaje

Citace BABIAK, Tomáš, Jan STREJČEK a Vojtěch ŘEHÁK. Almost linear Büchi automata. Mathematical Structures in Computer Science, Cambridge: Cambridge University Press, 2012, roč. 22, č. 2, s. 203-235. ISSN 0960-1295. doi:10.1017/S0960129511000399.
Originální název angličtina
Obor Informatika
WWW
Druh Článek v odborném periodiku
Klíčová slova LTL; linear time logic; model checking

Anotace

V článku zavádíme nový fragment logiky lineárního času (LTL) nazvaný LIO a dále také novou třídu Büchiho automatů (BA) nazývanou Almost linear Büchi automata (ALBA). Prezentujeme efektivní transformace mezi LIO a ALBA a ukazujeme tak, že tyto formalizmy mají stejnou vyjadřovací sílu. Protože očekáváme aplikace našich výsledků v oblasti model checkingu, používamé dva standardní zdroje specifikačních formulí (Spec Patterns a BEEM) k posouzení praktické relevance LIO fragmentu a k porovnání našeho překladu LIO na ALBA s dvojicí standardních překladů LTL na BA pomocí alternujících automatů. Na závěr ukazujeme, že překlad LIO na ALBA může být mnohem rychlejší než standardní překlad a může také produkovat podstatně menší automaty.

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

Další info