Linear Temporal Logic

Stream: Is there code for X?

[Mrigank Pawagi]

Hi all, I am an undergraduate student learning Lean in one of my classes. I am thinking of ideas for my course project (the requirements being that it should be doable in 40-50 days and useful to the lean community) and I am wondering if formalizing linear temporal logic would be a good idea.

I am aware of three such (and more or less unmaintained) Lean 3 projects, but none of them seem to have a Lean 4 port.

1. https://github.com/unitb/temporal-logic
2. https://github.com/loganrjmurphy/lean-temporal
3. https://github.com/James-Oswald/linear-temporal-logic

The first one also includes several results, like those in chapter 5 of the Model-checking book by Baier and Katoen. I am also planning to prove some of these results as part of my project (and if given time, I may extend my work beyond LTL to CTL).

My question to the lean Zulip community is whether any similar project for Lean 4 exists or is underway, and whether there are any specific results/features that I would be recommended to focus on.

Additionally, any references that I should check would be very useful! Thanks so much for your time :)

[Kyle Miller]

A grad student and I at UC Santa Cruz have a formalization underway for LTL, but it's not public yet. We're mostly focused on a library to use LTL for applications rather than a library to study LTL itself, though we're working on a bit of that too.

It seems possible that we'd both be approaching LTL somewhat differently, so it's possible that some overlap between projects is fine. Happy to talk about this with you and @Siddhartha Gadgil.

We're not doing CTL.

[Shreyas Srinivas]

I am working on a variant of CTL, but this has nothing to do with setting up the theory of LTL (not yet anyway). I do think that searching this zulip for either "LTL" or "CTL" will yield some interesting results since as far back as 2023 I recall people asking this question. The basic theory shouldn't be too hard, though I have no idea how difficult it is to formalise closure under complementation of Buchi automata.

[Mrigank Pawagi]

I found another nice implementation at https://github.com/GaloisInc/lean-protocol-support/tree/master/galois/temporal (but this is also Lean 3). This is all I could find on the Zulip chat besides the 3 projects I listed before.

Thanks @Kyle Miller for your response. I understand that you may not be able to share a lot of details at this moment, but it would be very helpful if you could provide some pointers on the scope of your project and therefore possible directions for me.

Thanks @Shreyas Srinivas! I think I will stick to LTL and try proving some automata-related results rather than working on CTL.

[Mrigank Pawagi]

Hi, a small update from my side: I started working on this project and have made some progress. For now, I am done with my "course project," but I plan to work more on this after the semester. At some point, I will make a post on this Zulip server to share the project broadly with people here. You can check it out at https://github.com/mrigankpawagi/LeanearTemporalLogic (the README has a detailed description of the state of the project). Thanks again!

[Siddhartha Gadgil]

Just one comment - it is good to have some easy theorems that check the correctness of definitions

[Mrigank Pawagi]

Sure, I will incorporate that – thanks!

[Ruben Van de Velde]

Can't stop my inner pedant: lemmae is not a standard plural of lemma - that would be lemmas or lemmata :)

[Mrigank Pawagi]

I remember my spell checker giving me red squiggly lines under "lemmae" and I thinking why the spell checker does not know this word! But yes you're right; I will fix that — thanks!