Rabinizer 2: small deterministic automata for LTL_
DOI10.1007/978-3-319-02444-8_32zbMATH Open1410.68231OpenAlexW4235354203MaRDI QIDQ5166706FDOQ5166706
Jan Křetínský, Ruslán Ledesma Garza
Publication date: 8 July 2014
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-319-02444-8_32
Recommendations
- Rabinizer: small deterministic automata for \({\mathrm{LTL}(\mathrm{F},\mathrm{G})}\)
- 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 (10)
- 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
- Functional Encryption for Inner Product with Full Function Privacy
- Rabinizer
- Extending Fairness Expressibility of ECTL+: A Tree-Style One-Pass Tableau Approach
- Generic Emptiness Check for Fun and Profit
- Optimal Translation of LTL to Limit Deterministic Automata
- From LTL to deterministic automata. A safraless compositional approach
- Efficient Analysis of Probabilistic Programs with an Unbounded Counter
- Guessing winning policies in LTL synthesis by semantic learning
Uses Software
This page was built for publication: Rabinizer 2: small deterministic automata for \(\mathrm{LTL}_{ \setminus\mathbf{GU}}\)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5166706)
