Effective translation of LTL to deterministic Rabin automata: beyond the ( F, G)-fragment
From MaRDI portal
(Redirected from Effective translation of LTL to deterministic Rabin automata: beyond the ( F, G)-fragment)
Effective translation of LTL to deterministic Rabin automata: beyond the \((\mathrm F,\mathrm G)\)-fragment
Effective translation of LTL to deterministic Rabin automata: beyond the \((\mathrm F,\mathrm G)\)-fragment
Abstract: Some applications of linear temporal logic (LTL) require to translate formulae of the logic to deterministic omega-automata. There are currently two translators producing deterministic automata: ltl2dstar working for the whole LTL and Rabinizer applicable to LTL(F,G) which is the LTL fragment using only modalities F and G. We present a new translation to deterministic Rabin automata via alternating automata and deterministic transition-based generalized Rabin automata. Our translation applies to a fragment that is strictly larger than LTL(F,G). Experimental results show that our algorithm can produce significantly smaller automata compared to Rabinizer and ltl2dstar, especially for more complex LTL formulae.
Recommendations
- Rabinizer: small deterministic automata for \({\mathrm{LTL}(\mathrm{F},\mathrm{G})}\)
- Comparison of LTL to Deterministic Rabin Automata Translators
- Rabinizer 3: Safraless translation of LTL to small deterministic automata
- A Unified Translation of Linear Temporal Logic to ω-Automata
- From LTL to deterministic automata. A safraless compositional approach
Cited in
(20)- LTL to self-loop alternating automata with generic acceptance and back
- First-order vs. second-order encodings for \textsc{ltl}\(_f\)-to-automata translation
- From LTL to deterministic automata. A safraless compositional approach
- Index appearance record with preorders
- Functional encryption for inner product with full function privacy
- How to translate efficiently extensions of temporal logics into alternating automata
- 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 deterministic Emerson-Lei automata
- Rabinizer 3: Safraless translation of LTL to small deterministic automata
- scientific article; zbMATH DE number 6527944 (Why is no real title available?)
- Generating deterministic -automata for most LTL formulas by the breakpoint construction
- Rabinizer: small deterministic automata for \({\mathrm{LTL}(\mathrm{F},\mathrm{G})}\)
- scientific article; zbMATH DE number 7455747 (Why is no real title available?)
- A Unified Translation of Linear Temporal Logic to ω-Automata
- One theorem to rule them all: a unified translation of LTL into -automata
- Rabinizer 2: small deterministic automata for \(\mathrm{LTL}_{ \setminus\mathbf{GU}}\)
- scientific article; zbMATH DE number 7649960 (Why is no real title available?)
- On the translation of automata to linear temporal logic
This page was built for publication: Effective translation of LTL to deterministic Rabin automata: beyond the \((\mathrm F,\mathrm G)\)-fragment
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5166674)
