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
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
- An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation
- A Compositional and Unified Translation of LTL into ω-Automata
- Converting Linear Temporal Logic to Deterministic (Generalized) Rabin Automata
- Converting Linear-Time Temporal Logic to Generalized Büchi Automata
- Promela Formalization
- Stuttering Equivalence