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.
- March 12, 2019
- Support for additional operators, implementation of common equivalence relations,
definition of syntactic fragments of LTL and the minimal disjunctive normal form.
- 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