A prototype using ltl2ldba (Owl) for quantitative model checking of MDPs (Markov decision process). Based on the PRISM model checker.


A tool for modal transition systems and their extensions supporting modal refinement checking and provides GUI for drawing.


A Java library for Omega-words, ω-automata and Linear Temporal Logic (LTL). Batteries included.

Rabinizer Verified (ltl2dra)

A tool constructing deterministic (generalized) Rabin Automata for LTL (Linear Time Logic). The implementation is extracted from the mechanically verified formalisation. The algorithm is compositional, safra-less, and yields small automata. A detailed description can be found in [1]. The tool itself is automatically extracted from the supplementary Isabelle/HOL theories, which are published in the Archive of Formal Proofs [2]. It is closely related to Rabinizer 3, since both tools implement the same algorithm and inspire each other. The only major difference is that LTL_to_DRA is formally verified, while Rabinizer 3 provides more features and has shorter running times.