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 PGSolver 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 3, and can be downloaded here.
- For more detail, see the Rabinizer 4 tool paper.
- It is built using Owl.
- Should you have any questions or suggestions, please contact {jan.kretinsky, tobias.meggendorfer, sickert} AT in.tum.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 precise definition of the input grammar can be found in FORMATS.md. Examples of valid formulas are:

`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"

- Rabinizer 3 can be found here.
- Rabinizer 2 (only supporting LTL\GU) can be found here.
- Rabinizer 1 (only supporting LTL with F- and G-operators) can be found 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.