Rabinizer: Small Deterministic Automata for LTL(F,G)
| Authors | |
|---|---|
| Year of publication | 2012 |
| Type | Article in Proceedings |
| Conference | Automated Technology for Verification and Analysis - 10th International Symposium ATVA 2012 |
| MU Faculty or unit | |
| Citation | |
| Doi | http://dx.doi.org/10.1007/978-3-642-33386-6_7 |
| Field | Informatics |
| Keywords | linear temporal logic; automata; determinism |
| Description | We present Rabinizer, a tool for translating formulae of the fragment of linear temporal logic with the operators $\F$ (eventually) and $\G$ (globally) into deterministic Rabin automata. Contrary to tools like ltl2dstar, which translate the formula into a B\"uchi automaton and apply Safra's determinization procedure, Rabinizer uses a direct construction based on the logical structure of the formulae. We describe a number of optimizations of the basic procedure, crucial for the good performance of Rabinizer, and present an experimental comparison. |
| Related projects: |