Translation of LTL to Büchi Automata: Improved Once Again
| Authors | |
|---|---|
| Year of publication | 2010 |
| Type | Article in Proceedings |
| Conference | Proceedings of 9th International Summer School on Modelling and Verifying Parallel Processes 2010 (MOVEP 2010) |
| MU Faculty or unit | |
| Citation | |
| Field | Informatics |
| Keywords | LTL; linear time logic; translation of LTL; Büchi Automata; model checking |
| Description | We present an improvement of an algorithm translating LTL formulae into Büchi automata via alternating automata. In particular, we improve the transformation of alternating Büchi automata to generalized Büchi automata, where we temporarily ignore some transitions leading from the alternating automata states corresponding to subformulae that are prefix-invariant. Experimental results show that our improvements can lead to faster translation and less nondeterminism of the resulting Büchi automata. |
| Related projects: |