Rabinizer

MaRDI QIDQ32821swMATHFDO

Official website https://www7.in.tum.de/~kretinsk/rabinizer3.html

Described by source

• Rabinizer 2: small deterministic automata for \(\mathrm{LTL}_{ \setminus\mathbf{GU}}\)
• Rabinizer 3: Safraless translation of LTL to small deterministic automata
• Rabinizer: small deterministic automata for \({\mathrm{LTL}(\mathrm{F},\mathrm{G})}\)

Cited in

(28)

• Seminator 2
• ProbDiVinE
• LiQuor
• Branching-time logic \(\mathsf{ECTL}^{\#}\) and its tree-style one-pass tableau: extending fairness expressibility of \(\mathsf{ECTL}^+\)
• Back to the future: a fresh look at linear temporal logic
• SPOT
• BEEM
• LTL2BA
• From LTL to deterministic automata. A safraless compositional approach
• TTM
• PGSolver
• Index appearance record with preorders
• Model checking probabilistic systems
• ltl2dstar
• Generic emptiness check for fun and profit
• Index appearance record for transforming Rabin automata into parity automata
• Optimal Translation of LTL to Limit Deterministic Automata
• LTL_to_DRA
• Strix
• Limit-deterministic Büchi automata for linear temporal logic
• A Unified Translation of Linear Temporal Logic to ω-Automata
• Extending fairness expressibility of ECTL^+: a tree-style one-pass tableau approach
• One theorem to rule them all: a unified translation of LTL into -automata
• Efficient analysis of probabilistic programs with an unbounded counter
• Near-linear time algorithms for Streett objectives in graphs and MDPs
• MoChiBA
• Owl
• JBDD

This page was built for software: Rabinizer