Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata

DOI10.1007/978-3-319-11936-6_17zbMath1448.68268OpenAlexW141312837MaRDI QIDQ3457793

Zuzana Komárková, Jan Křetínský

Publication date: 17 December 2015

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-11936-6_17

Mathematics Subject Classification ID

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

Related Items (9)

From LTL to deterministic automata. A safraless compositional approach ⋮ Model Checking Probabilistic Systems ⋮ Index appearance record with preorders ⋮ 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 ⋮ Rabinizer

Uses Software

• PRISM
• SPOT
• LTL2BA
• ltl2dstar

This page was built for publication: Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata