Rabinizer 4 is a tool set for generating small deterministic ω-automata from LTL (linear temporal logic) formulas
bin/ltl2dpa "GFa & GFb"
translates the LTL formula GFa ∧ GFb into a deterministic parity automaton. The commandbin/ltl2dgra --annotations "GFa & GF(b & X!b)"
translates the LTL formula GFa ∧ GF(b ∧ X¬b) into a deterministic generalized Rabin automaton, labelling its states with their logical semantics. This command replaces previous versions of Rabinizer.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:
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"
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.