Almost linear Büchi automata
| Authors | |
|---|---|
| Year of publication | 2012 |
| Type | Article in Periodical |
| Magazine / Source | Mathematical Structures in Computer Science |
| MU Faculty or unit | |
| Citation | |
| Web | http://dx.doi.org/10.1017/S0960129511000399 |
| Doi | http://dx.doi.org/10.1017/S0960129511000399 |
| Field | Informatics |
| Keywords | LTL; linear time logic; model checking |
| Description | 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. |
| Related projects: |
|