Temporal Logic

Stream: Is there code for X?

[Graham Leach-Krouse]

Is there any notable recent work on embedding temporal logic(s) in Lean?

I noticed this: https://lean-forward.github.io/lean-together/2019/slides/hudon.pdf

But I don't have any more recent references.

[Patrick Massot]

@Simon Hudon :up:

[Simon Hudon]

Here is the code for that project: https://github.com/unitb/temporal-logic

It's a bit old. I've been meaning to keep it up to date with mathlib and lean but I haven't had time in a while.

[Utensil Song]

Here are some projects I found previously about reasoning with concurrent/distributed systems in Lean, in reverse chronological order:

• https://github.com/leanprover-community/iris-lean (updated: 3 weeks ago)
  • has: Higher-Order Concurrent Separation Logic
  • ref: https://iris-project.org/
• https://github.com/loganrjmurphy/lean-temporal (updated: Nov 11, 2020)
  • has: LTL (Linear Temporal Logic) + CTL (Computational Tree Logic)
  • ref: Baier, Christel, and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008
• https://github.com/unitb/temporal-logic (updated: Nov 1, 2018)
  • has: LTL + refinement
  • ref: https://lean-forward.github.io/lean-together/2019/slides/hudon.pdf
  • see also:
    • its usage in unitb-semantics, ref: https://arxiv.org/abs/1810.10143
    • separation-logic
• https://github.com/GaloisInc/lean-protocol-support/tree/master/galois/temporal (updated: Sep 22, 2017)
  • has: LTL + LTS (Labelled Transition System)
  • ref: Roberto Gorrieri. Process Algebras for Petri Nets: The Alphabetization of Distributed Systems. Springer, 2017

Actually, only the last three match the topic, and they're all in Lean 3 .

[Graham Leach-Krouse]

Thanks both! Very much appreciated.

[Malvin Gattinger]

Did you already start working on this or found more related work? I am interested in Modal Logic in general and sometimes I dream of a general way to embed Modal (or also other Logics) in Lean / Mathlib. For Basic Modal Logic I clumsily formalized a tableaux system as my first Lean 3 project https://github.com/m4lvin/tablean and my long-term goal is to cover Propositional Dynamic Logic (also after switching to Lean 4).