Rabinizer 3 is a tool generating small deterministic Rabin automata and even smaller deterministic generalized Rabin automata from LTL formulae. It is free and open source. You can download both the tool and its source code for free below. Distribution is under the GNU General Public License (GPL), version 2. The tool has been tested using ltlcross. The algorithm implemented has been proven correct in Isabelle. For questions please contact Jan Kretinsky.

References in zbMATH (referenced in 10 articles , 3 standard articles )

Showing results 1 to 10 of 10.
Sorted by year (citations)

  1. Bolotov, Alexander; Hermo, Montserrat; Lucio, Paqui: Branching-time logic (\mathsfECTL^#) and its tree-style one-pass tableau: extending fairness expressibility of (\mathsfECTL^+) (2020)
  2. Baier, Christel; Blahoudek, František; Duret-Lutz, Alexandre; Klein, Joachim; Müller, David; Strejček, Jan: Generic emptiness check for fun and profit (2019)
  3. Baier, Christel; de Alfaro, Luca; Forejt, Vojtěch; Kwiatkowska, Marta: Model checking probabilistic systems (2018)
  4. Kini, Dileep; Viswanathan, Mahesh: Optimal translation of LTL to limit deterministic automata (2017)
  5. Křetínský, Jan; Meggendorfer, Tobias; Waldmann, Clara; Weininger, Maximilian: Index appearance record for transforming Rabin automata into parity automata (2017)
  6. Esparza, Javier; Křetínský, Jan; Sickert, Salomon: From LTL to deterministic automata. A safraless compositional approach (2016)
  7. Brázdil, Tomás; Kiefer, Stefan; Kŭcera, Antonín: Efficient analysis of probabilistic programs with an unbounded counter (2014)
  8. Komárková, Zuzana; Křetínský, Jan: Rabinizer 3: Safraless translation of LTL to small deterministic automata (2014)
  9. Křetínský, Jan; Ledesma Garza, Ruslán: Rabinizer 2: small deterministic automata for (\mathrmLTL_ \setminus\mathbfGU) (2013)
  10. Gaiser, Andreas; Křetínský, Jan; Esparza, Javier: Rabinizer: small deterministic automata for (\mathrmLTL(\mathrmF,\mathrmG)) (2012)