A Verified and Compositional Translation of LTL to Deterministic Rabin Automata. - Julian Brunner 001; Benedikt Seidl; Salomon Sickert (ITP, 2019)

A Compositional and Unified Translation of LTL into ω-Automata. - Benedikt Seidl; Salomon Sickert (Arch. Formal Proofs, 2019)