Title: On Inductive and co-inductive interpretations for LTL proof systems

Abstract:

In this talk I will present a study on the relationship between LTL (model-based) semantics and its respective proof-theoretic interpretations.  I identify descrepancies between the various interpretations and illustrate them using examples.  My formal treatment also allows me to prove certain corresponencies between the various semantics.  In particular, I investigate both inductive and coinductive interpretations of the logic. The coinductive interpretation appears to be relatively novel and is motivated, in part, by the model over which the logic (LTL) is defined i.e. infinite strings.  It should also lend itself more naturally to the formalisation of runtime verification algorithms for the logic, which can be given an extensional flavour.