### Abstract

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 than 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.

### License

BSD License

### History

March 24, 2016
  Make use of the LTL entry and include the simplifier.
September 23, 2015
  Enable code export for the eager unfolding optimisation and reduce running time of the generated tool. Moreover, add support for the mlton SML compiler.

### Topics

- Computer science/Automata and formal languages

### Session LTL_to_DRA

- Preliminaries2
- Map2
- Mapping2
- DTS
- Semi_Mojmir
- Mojmir
- Rabin
- List2
- Mojmir_Rabin
- LTL_FGXU
- af
- Logical_Characterization
- LTL_Rabin
- LTL_Rabin_Unfold_Opt
- LTL_Compat
- LTL_Impl
- af_Impl
- Mojmir_Rabin_Impl
- LTL_Rabin_Impl
- Export_Code

### Depends on

- Boolean Expression Checkers
- Knowledge-based programs
- Linear Temporal Logic
- List Index

## Cite

×

LTL_to_DRA-AFP

    @article{LTL_to_DRA-AFP,
      author  = {Salomon Sickert},
      title   = {Converting Linear Temporal Logic to Deterministic (Generalized) Rabin Automata},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2015},
      note    = {\url{https://isa-afp.org/entries/LTL_to_DRA.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- Sep 4, 2015 : Isabelle2015