Linear Temporal Logic

 

Title: Linear Temporal Logic
Author: Salomon Sickert (s /dot/ sickert /at/ tum /dot/ de)
Contributor: Benedikt Seidl (benedikt /dot/ seidl /at/ tum /dot/ de)
Submission date: 2016-03-01
Abstract: This theory provides a formalisation of linear temporal logic (LTL) and unifies previous formalisations within the AFP. This entry establishes syntax and semantics for this logic and decouples it from existing entries, yielding a common environment for theories reasoning about LTL. Furthermore a parser written in SML and an executable simplifier are provided.
Change history: [2019-03-12]: Support for additional operators, implementation of common equivalence relations, definition of syntactic fragments of LTL and the minimal disjunctive normal form.
BibTeX:
@article{LTL-AFP,
  author  = {Salomon Sickert},
  title   = {Linear Temporal Logic},
  journal = {Archive of Formal Proofs},
  month   = mar,
  year    = 2016,
  note    = {\url{http://isa-afp.org/entries/LTL.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Boolean_Expression_Checkers
Used by: LTL_Master_Theorem, LTL_to_DRA, LTL_to_GBA, Promela, Stuttering_Equivalence