Contribution: LTL

Linear Temporal Logic

Authors

Description

This contribution contains a shallow embedding of Linear Temporal Logic (LTL) based on a co-inductive representation of program executions. Temporal operators are implemented as inductive (respectively co-inductive) types when they are least (respectively greatest) fixpoints. Several general lemmas, that correspond to LTL rules, are proved.

Keywords

temporal logic, infinite transition systems, co induction

README

 Here is a shallow embedding of linear temporal logic (LTL). 
Program executions are represented by infinite co-inductive lists 
and  temporal operators by co-inductive or inductive types, 
depending on whether they are greatest or least fixpoints.

ltl.v contains a parameterized specification of infinite transitions systems, 
the definitions of LTL operators and some safety and fairness related notions.

The other files contain lemmas corresponding to LTL rules. 

Contents:

safety.v  : co-inductive lemmas that correspond to safety properties
liveness.v : inductive lemmas that correspond to liveness properties
fairness.v : a comparison between two notions of fairness
congruence.v : the monotonicity of temporal operators
leads_to.v : some transition properties of ``leads_to_via''
termination.v : the main termination lemma. It makes it possible to conclude that, 
provided that a property  A initially holds on a stream, 
a property B continuously holds  until a property C is eventually satisfied. 
The proof is based on the existence of a measure on the states ranging over 
a set equipped with a well-founded relation. It is assumed that eventually, 
either the measure strictly decreases, or  C becomes true. Meanwhile, B remains true.

Available files