Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment

DOI10.1007/978-3-319-02444-8_4zbMath1414.03003arXiv1306.4636OpenAlexW1909185322MaRDI QIDQ5166674

František Blahoudek, Jan Strejček, Tomáš Babiak, Mojmír Křetínský

Publication date: 8 July 2014

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1306.4636

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Temporal logic (03B44)

Related Items (10)

From LTL to deterministic automata. A safraless compositional approach ⋮ Index appearance record with preorders ⋮ Unnamed Item ⋮ LTL to self-loop alternating automata with generic acceptance and back ⋮ Unnamed Item ⋮ Unnamed Item ⋮ 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 ⋮ Functional Encryption for Inner Product with Full Function Privacy

Uses Software

• LTL2BA

This page was built for publication: Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment