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.
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 . The tool itself is automatically extracted from the supplementary Isabelle/HOL theories, which are published in the Archive of Formal Proofs . 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.