Linear Temporal Logic

Salomon Sickert 🌐 with contributions from Benedikt Seidl 📧

March 1, 2016

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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.

License

BSD License

History

March 12, 2019
Support for additional operators, implementation of common equivalence relations, definition of syntactic fragments of LTL and the minimal disjunctive normal form.

Topics

Session LTL

Depends on

Used by

Cite

× 
@article{LTL-AFP,
  author  = {Salomon Sickert},
  title   = {Linear Temporal Logic},
  journal = {Archive of Formal Proofs},
  month   = {March},
  year    = {2016},
  note    = {\url{https://isa-afp.org/entries/LTL.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: