Rabinizer 4 is a tool set for generating small deterministic ω-automata from LTL (linear temporal logic) formulas

- It translates LTL to various types of automata, e.g. (generalized) Rabin, parity, or limit-deterministic Büchi.
- It is linked to the probabilistic model checker PRISM and a parity-game solver PGSolve and thus can be used for probabilistic model checking and for synthesis.
- It is free and open source, distributed under the GNU General Public License (GPL), version 2, and can be downloaded here.
- For more detail, see the Rabinizer 4 tool paper.
- Should you have any questions or suggestions, please contact {jan DOT kretinsky, tobias DOT meggendorfer, salomon DOT sickert} AT in DOT tum DOT de.

bin/ltl2dpa "GFa & GFb"

translates the LTL formulabin/ltl2dgra --annotations "GFa & GF(b & X!b)"

translates the LTL formula- ltl2dra -- translates LTL to deterministic Rabin automata
- ltl2dgra -- translates LTL to deterministic generalized Rabin automata
- ltl2ldba -- translates LTL to limit-deterministic Büchi automata
- ltl2ldgba -- translates LTL to limit-deterministic generalized Büchi automata
- ltl2dpa -- translates LTL to deterministic parity automata
- fltl2dgmra -- translates the frequency extension of LTL to deterministic generalized mean-payoff Rabin automata

bin/ltl2dgra ‹formula›

where *‹formula›* is an LTL formula using operators `X`, `F`, `G`, `W`, `R`, `M`, `U`, `!`, `&`, `∣`, atomic propositions (alphanumeric string starting with a lowercase letter), parentheses, `true`, `false`, and some more.
A more formal definition by an ANTLR grammar can be found in the source code (`src/main/antlr`).
Examples of valid formulas:

`F G (a | b U c) & !a U (b U X c)``G F a & G F b``((F G reset) | (G F loc2)) & G test & ! G wait & init``(G F a XOR G b) <-> ((a R c) W (G F d))`

The above call outputs a transition-based generalized Rabin automaton in the HOA format.
This automaton can be converted to the popular dot format by piping it to `autfilt --dot`.
Dot files can be viewed by dot-viewers, such as XDot, or rendered to PNG / SVG by further piping to the dot executable (`dot -Tpng` / `dot -Tsvg`).
To include semantic labelling, add `--annotations` as the **first** parameter.
For example, to obtain an image of a DGRA recognizing the formula a ∨ **G** b, execute the following command (on Linux):

bin/ltl2dgra --annotations "a | G b" | autfilt --dot | dot -Tpng > automaton.png

The input set can also be read from and written to files as follows:

bin/ltl2dgra --annotations -I "input.ltl" -O "output.hoa"

- From LTL to Deterministic Automata: A Safraless Compositional Approach (CAV'14)
- Limit-Deterministic Büchi Automata for Linear Temporal Logic (CAV'16)
- From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata (TACAS'17)
- Index appearance record for transforming Rabin automata into parity automata (TACAS'17)
- Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata (ATVA'14, previous version of the tool)

The previous version Rabinizer 3 can be found here. The older version of the tool for the fragment of LTL with F and G operators can be found here and for the fragment LTL\GU here.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS ''AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.