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