Informace o publikaci

Almost linear Büchi automata

Název česky Skoro lineární Büchiho automaty
Autoři

BABIAK Tomáš STREJČEK Jan ŘEHÁK Vojtěch

Druh Článek v odborném periodiku
Časopis / Zdroj Mathematical Structures in Computer Science
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
WWW http://dx.doi.org/10.1017/S0960129511000399
Doi http://dx.doi.org/10.1017/S0960129511000399
Obor Informatika
Klíčová slova LTL; linear time logic; model checking
Popis 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.
Související projekty:

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

Další info