Email Gateway (Aug 22 2022 at 11:24): Email Gateway (Aug 22 2022 at 11:24):From: Larry Paulson <lp15@cam.ac.uk>
AFP entries keep coming in! This one is a substantial development for translating LTL formulas into automata.
Converting Linear Temporal Logic to Deterministic (Generalised) Rabin Automata
Salomon Sickert
Recently, Javier Esparza and Jan Kretinsky proposed a new method directly translating linear temporal logic (LTL) formulas to deterministic (generalized) Rabin automata. Compared to the existing approaches of constructing a non-deterministic Buechi-automaton in the first step and then applying a determinization procedure (e.g. some variant of Safra's construction) in a second step, this new approach preservers a relation between the formula and the states of the resulting automaton. While the old approach produced a monolithic structure, the new method is compositional. Furthermore, in some cases the resulting automata are much smaller then the automata generated by existing approaches. In order to ensure the correctness of the construction, this entry contains a complete formalisation and verification of the translation. Furthermore from this basis executable code is generated.
AFP entry: http://afp.sourceforge.net/entries/LTL_to_DRA.shtml
Larry
Last updated: Apr 20 2024 at 08:16 UTC