Skip to content

Instantly share code, notes, and snippets.

@koehlma

koehlma/ltl.v

Created March 10, 2017 12:32
Show Gist options
  • Save koehlma/5224a6d9f8c29c46f647ff679f273da6 to your computer and use it in GitHub Desktop.
Save koehlma/5224a6d9f8c29c46f647ff679f273da6 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
ltl.v
Require Import Relations.
Set Implicit Arguments.
Section LTL.
Variable State : Type.
(* Traces *)
CoInductive Trace : Type :=
| Cons : State -> Trace -> Trace.
Definition head (trace : Trace) :=
match trace with Cons head tail => head end.
Definition tail (trace : Trace) :=
match trace with Cons head tail => tail end.
(* Formulas *)
Definition TraceFormula := Trace -> Prop.
Definition StateFormula := State -> Prop.
(* Operators *)
Definition next (F : TraceFormula) : TraceFormula :=
fun trace => F (tail trace).
Definition and (F : TraceFormula) (G : TraceFormula) : TraceFormula :=
fun trace => (F trace) /\ (G trace).
Definition or (F : TraceFormula) (G : TraceFormula) : TraceFormula :=
fun trace => (F trace) \/ (G trace).
Definition equiv (F : TraceFormula) (G : TraceFormula) : TraceFormula :=
fun trace => (F trace) <-> (G trace).
Definition not (F : TraceFormula) : TraceFormula :=
fun trace => (F trace) -> False.
Definition implies (F : TraceFormula) (G : TraceFormula) : TraceFormula :=
fun trace => (F trace) -> (G trace).
CoInductive globally (F : TraceFormula) : Trace -> Prop :=
| globally_I trace: F trace -> globally F (tail trace) -> globally F trace.
Inductive eventually (F : TraceFormula) : Trace -> Prop :=
| eventually_B trace: F trace -> eventually F trace
| eventually_S trace: eventually F (tail trace) -> eventually F trace.
Inductive until (F : TraceFormula) (G : TraceFormula) : Trace -> Prop :=
| until_B trace: G trace -> until F G trace
| until_S trace: F trace -> until F G (tail trace) -> until F G trace.
End LTL.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment