Rabinizer: small deterministic automata for LTL(F,G)

DOI10.1007/978-3-642-33386-6_7MaRDI QIDQ4649288zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Temporal logic (03B44) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

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

Cited in

(9)

• Back to the future: a fresh look at linear temporal logic
• From LTL to deterministic automata. A safraless compositional approach
• Rabinizer
• Index appearance record for transforming Rabin automata into parity automata
• Rabinizer 3: Safraless translation of LTL to small deterministic automata
• A Unified Translation of Linear Temporal Logic to ω-Automata
• Effective translation of LTL to deterministic Rabin automata: beyond the \((\mathrm F,\mathrm G)\)-fragment
• Rabinizer 2: small deterministic automata for \(\mathrm{LTL}_{ \setminus\mathbf{GU}}\)
• Guessing winning policies in LTL synthesis by semantic learning

Describes a project that uses

Uses Software

• PRISM
• BEEM
• LTL2BA
• ltl2dstar

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)