Almost linear Büchi automata

Logo poskytovatele
Logo poskytovatele
Logo poskytovatele
Logo poskytovatele
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 Skoro lineární Büchiho automaty
Autoři

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

Rok publikování 2012
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.