Identifikační kód | RIV/00216224:14330/12:00057181 |
Název v anglickém jazyce | Almost linear Büchi automata |
Druh | J - Článek v odborném periodiku |
Jazyk | eng - angličtina |
Obor - skupina | I - Informatika |
Obor | IN - Informatika |
Rok uplatnění | 2012 |
Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
Počet výskytů výsledku | 2 |
Počet tvůrců celkem | 3 |
Počet domácích tvůrců | 3 |
Výčet všech uvedených jednotlivých tvůrců | Tomáš Babiak (státní příslušnost: SK - Slovenská republika, domácí tvůrce: A, vedidk: 9653023) Jan Strejček (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 3978915) Vojtěch Řehák (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 8986371) |
Popis výsledku v anglickém jazyce | We introduce a new fragment of Linear temporal logic (LTL) called LIO and a new class of Büchi automata (BA) called Almost linear Büchi automata (ALBA). We provide effective translations between LIO and ALBA showing that the two formalisms are expressively equivalent. As we expect applications of our results in model checking, we use two standard sources of specification formulae, namely Spec Patterns and BEEM, to study practical relevance of LIO fragment, and to compare our translation of LIO to ALBA with two standard translations of LTL to BA via alternating automata. Finally, we demonstrate that the LIO to ALBA translation can be much faster than the standard translation and the produced automata can be substantially smaller. |
Klíčová slova oddělená středníkem | LTL; linear time logic; model checking |
Stránka www, na které se nachází výsledek | - |
DOI výsledku | 10.1017/S0960129511000399 |