Rabinizer: small deterministic automata for LTL(F,G)
DOI10.1007/978-3-642-33386-6_7zbMATH Open1374.68259OpenAlexW2293285880MaRDI QIDQ4649288FDOQ4649288
Authors: Andreas Gaiser, Jan Křetínský, Javier Esparza 
Publication date: 21 November 2012
Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-33386-6_7
Recommendations
- Rabinizer 2: small deterministic automata for \(\mathrm{LTL}_{ \setminus\mathbf{GU}}\)
- Rabinizer 3: Safraless translation of LTL to small deterministic automata
- Effective translation of LTL to deterministic Rabin automata: beyond the \((\mathrm F,\mathrm G)\)-fragment
- Comparison of LTL to Deterministic Rabin Automata Translators
- From LTL to deterministic automata. A safraless compositional approach
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Cited In (9)
- A Unified Translation of Linear Temporal Logic to ω-Automata
- Back to the future: a fresh look at linear temporal logic
- Index appearance record for transforming Rabin automata into parity automata
- Rabinizer
- From LTL to deterministic automata. A safraless compositional approach
- Effective translation of LTL to deterministic Rabin automata: beyond the \((\mathrm F,\mathrm G)\)-fragment
- Guessing winning policies in LTL synthesis by semantic learning
- Rabinizer 2: small deterministic automata for \(\mathrm{LTL}_{ \setminus\mathbf{GU}}\)
- Rabinizer 3: Safraless translation of LTL to small deterministic automata
Uses Software
This page was built for publication: Rabinizer: small deterministic automata for \({\mathrm{LTL}(\mathrm{F},\mathrm{G})}\)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4649288)
