PV1 ⊧ Rabinizercan translate LTL formulae into different types of automata

A tool set for translating formulae of LTL to different types of deterministic ω-automata.

Application domain/field

• Linear temporal logic (LTL)
• Deterministic 𝜔-automata
• Rabin automata
• Büchi automata
• Automata translation

Type of tool

Automata translator

Expected input

LTL formula

Format:

Same format as Owl, described in detail here: https://gitlab.lrz.de/i7/owl/blob/master/doc/FORMATS.md

Expected output

Automata that corresponds to the LTL formula.

Internals

As of Rabinizer 4, it can translate an LTL formula into one of the following type of automata:

• DGRA: deterministic generalized Rabin automata
• DRA: deterministic Rabin automata
• DPA: deterministic parity automata
• LDGBA: limit-deterministic generalized Büchi automata
• LDBA: limit-deterministic Büchi automata
• Or it can translate the frequency extension of LTL to a deterministic generalized mean-payoff Rabin automata (DGRMA)

It is also linked to PRISM to allow for probabilistic verification of some automata.

Comments

Bundled with Owl, a tool collection and library for Omega-words, 𝜔-automata and Linear Temporal Logic (LTL). https://owl.model.in.tum.de/