Email Gateway (Aug 22 2022 at 19:27): Email Gateway (Aug 22 2022 at 19:27):From: Tobias Nipkow <nipkow@in.tum.de>
A Compositional and Unified Translation of LTL into ω-Automata
Benedikt Seidl and Salomon Sickert
We present a formalisation of the unified translation approach of linear
temporal logic (LTL) into ω-automata from [1]. This approach decomposes LTL
formulas into ``simple'' languages and allows a clear separation of concerns:
first, we formalise the purely logical result yielding this decomposition;
second, we instantiate this generic theory to obtain a construction for
deterministic (state-based) Rabin automata (DRA). We extract from this
particular instantiation an executable tool translating LTL to DRAs. To the best
of our knowledge this is the first verified translation from LTL to DRAs that is
proven to be double exponential in the worst case which asymptotically matches
the known lower bound.
[1] Javier Esparza, Jan Kretínský, Salomon Sickert. One Theorem to Rule Them
All: A Unified Translation of LTL into ω-Automata. LICS 2018
https://www.isa-afp.org/entries/LTL_Master_Theorem.html
Enjoy!
smime.p7s
Last updated: Apr 18 2024 at 12:27 UTC