Rabinizer: Small Deterministic Automata for LTL(F,G)
| Autoři | |
|---|---|
| Rok publikování | 2012 |
| Druh | Článek ve sborníku |
| Konference | Automated Technology for Verification and Analysis - 10th International Symposium ATVA 2012 |
| Fakulta / Pracoviště MU | |
| Citace | |
| Doi | http://dx.doi.org/10.1007/978-3-642-33386-6_7 |
| Obor | Informatika |
| Klíčová slova | linear temporal logic; automata; determinism |
| Popis | 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. |
| Související projekty: |