![Důležité termíny](https://cdn.muni.cz/media/3633704/image_2.jpg?mode=crop¢er=0.5,0.5&rnd=133572412150000000&heightratio=0.5&width=278)
Informace o publikaci
Almost linear Büchi automata
Název česky | Skoro lineární Büchiho automaty |
---|---|
Autoři | |
Rok publikování | 2012 |
Druh | Článek v odborném periodiku |
Časopis / Zdroj | Mathematical Structures in Computer Science |
Fakulta / Pracoviště MU | |
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: |
|