Model Checking

Stream: new members

[Marcus Rossel]

I'm currently reading Principles of Model Checking and am considering formalizing some of its material.
Does anyone know if there are any model checking related formalizations out there (or in Mathlib) yet?
That is, things like transition systems, state graphs, traces, linear time properties, ...

[Logan Murphy]

I have a very bare-bones formalization of LTL and CTL based on that book, you can see here.

I know that Simon Hudon gave a talk at LT19 about embedding temporal logics, I believe these are the slides. I also think there was some talk about these in the #Program verification stream a while ago.

edit : see https://leanprover.zulipchat.com/#narrow/stream/236449-Program-verification/topic/Projects/near/215764510

I don't know of anyone who did a more significant formalization of that book's material though.

[Logan Murphy]

Another thing I started playing with recently was porting John Harrsion's OCaml code on model checking to Lean 4, although this has been put on the back burner for a while