### Abstract

We formalize linear-time temporal logic (LTL) and the algorithm by Gerth et al. to convert LTL formulas to generalized Büchi automata. We also formalize some syntactic rewrite rules that can be applied to optimize the LTL formula before conversion. Moreover, we integrate the Stuttering Equivalence AFP-Entry by Stefan Merz, adapting the lemma that next-free LTL formula cannot distinguish between stuttering equivalent runs to our setting.

We use the Isabelle Refinement and Collection framework, as well as the Autoref tool, to obtain a refined version of our algorithm, from which efficiently executable code can be extracted.

### License

BSD License

### Topics

- Computer science/Automata and formal languages

### Session LTL_to_GBA

- LTL_to_GBA
- LTL_to_GBA_impl
- All_Of_LTL_to_GBA

### Depends on

- The CAVA Automata Library
- Linear Temporal Logic
- Stuttering Equivalence

### Used by

- A Fully Verified Executable LTL Model Checker

### Auto-related entries

- A Separation Logic Framework for Imperative HOL

## Cite

×

LTL_to_GBA-AFP

    @article{LTL_to_GBA-AFP,
      author  = {Alexander Schimpf and Peter Lammich},
      title   = {Converting Linear-Time Temporal Logic to Generalized Büchi Automata},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/LTL_to_GBA.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
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- May 29, 2014 : Isabelle2013-2