Name
Abstract | ||
|---|---|---|
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 there to be applications of our results in model checking, we use two standard sources of specification formulae, namely Spec Patterns and BEEM, to study the practical relevance of the LIO fragment, and to compare our translation of LIO to ALBA with two standard translations of LTL to BA using alternating automata. Finally, we demonstrate that the LIO to ALBA translation can be much faster than the standard translation, and the resulting automata can be substantially smaller. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1017/S0960129511000399 | Electronic Proceedings in Theoretical Computer Science |
Keywords | DocType | Volume |
standard source,standard translation,new fragment,linear temporal logic,new class,linear b,alba translation,effective translation,lio fragment,chi automaton | Journal | 22 |
Issue | ISSN | Citations |
2 | 0960-1295 | 2 |
PageRank | References | Authors |
0.36 | 13 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tomáš Babiak | 1 | 90 | 3.70 |
| Vojtĕch Řehák | 2 | 36 | 5.15 |
| Jan Strejček | 3 | 79 | 8.12 |