Model Checking

Stream: Program verification

[Marcus Rossel]

Hey all :wave: I'm interested in working on integrating model checking with Lean (in what exact form is yet to be determined). So I was wondering what the current state of model checking in Lean is? The only related threads I've found are:

• new members > Model Checking
• general > Model checking in Lean
• Program verification > Projects

In these threads there are various examples of people having developed certain parts of temporal logics in Lean, but no model checking algorithms or integration with existing model checkers.
If things have changed wrt. model checking since those threads were started I would love to hear about it!

[Shreyas Srinivas]

Marcus Rossel said:

Hey all :wave: I'm interested in working on integrating model checking with Lean (in what exact form is yet to be determined). So I was wondering what the current state of model checking in Lean is? The only related threads I've found are:

• new members > Model Checking
• general > Model checking in Lean
• Program verification > Projects

In these threads there are various examples of people having developed certain parts of temporal logics in Lean, but no model checking algorithms or integration with existing model checkers.
If things have changed wrt. model checking since those threads were started I would love to hear about it!

I think the issue that will bother you first when you try to add model checking algorithms is that there is no agreement on how to add algorithms to Lean.

[Shreyas Srinivas]

There are different people pursuing different approaches in the Computational Complexity thread in the general stream

[Shreyas Srinivas]

There was also another thread about checking that DFS works (i.e. all nodes are visited), by @Anand Rao who might know more about that.

[Shreyas Srinivas]

There was also this PR : https://github.com/leanprover-community/mathlib4/pull/3221

[Shreyas Srinivas]

The isabelle community has some algorithm verification people who have developed frameworks for this. For example : https://dl.acm.org/doi/10.1145/2676724.2693165

[Shreyas Srinivas]

I can't say much about other aspects of model checking. The computability section of mathlib has some machinery for automaton, but I haven't found any description of Buchi automata yet, to give one example.

[Marcus Rossel]

Wow, thanks @Shreyas Srinivas! My rough idea was to call a model checker (like SPIN, PRISM, ...) from Lean and somehow use verification witnesses to generate proofs in Lean. Then I wouldn't have to implement the model checking algorithms myself. Though I don't know how much model checking theory would need to be defined in order to turn verification witnesses into proofs.

[Shreyas Srinivas]

Marcus Rossel said:

Wow, thanks Shreyas Srinivas! My rough idea was to call a model checker (like SPIN, PRISM, ...) from Lean and somehow use verification witnesses to generate proofs in Lean. Then I wouldn't have to implement the model checking algorithms myself. Though I don't know how much model checking theory would need to be defined in order to turn verification witnesses into proofs.

In principle one part of this is similar to a hammer for lean, except this hammer calls verification tools rather than SMT solvers. You might want to check those threads.

The other part is interpreting certificates. You will need the relevant theories in which you analyse the certificates. There is a thread on Separation Logics for example ,which points to a (presently unmaintained) library of separation logic that is a port of Coq's Iris.

[Shreyas Srinivas]

And there are might be other similar libraries for some other logics as you point out.

A lot depends on what level of verification you are looking for : Presumably you will need to implement the algorithms in the paper itself, but you could argue that you trust your implementation and not verify their correctness in lean. Or you could carefully implement and verify them in lean.

[Andrés Goens]

Shreyas Srinivas said:

The other part is interpreting certificates. You will need the relevant theories in which you analyse the certificates. There is a thread on Separation Logics for example ,which points to a (presently unmaintained) library of separation logic that is a port of Coq's Iris.

oh interesting that you mention that, what's the relationship between separation logic and model checking/temporal logics? is there an obvious connection there that I'm missing?

[Andrés Goens]

There's also some verified implementation of some basic model checking algorithms in Coq too, like this or this. An option is to have a verified basic version in Lean and an unverified external version (say, through an FFI or just calling the programs) to a mature model checker like SPIN or PRISM, so you can re-check minimal subsystems that those return, or where you can decide wether or not to trust the external tool, like is done e.g. with GMP currently

[Gary Haussmann]

This thread is timely for me because I recently went through the first half of "Principles of Model Checking" textbook (stopping just short of CTL* and Bisimulation) and wrote up most of the algorithms in Lean. I also wrote up a simple widget to visualize transition systems in VSCode.
https://gitlab.com/Izzimach/solifugid-z

However since my background is systems programming and not theorem-proving all my Lean code is just algorithms with no proofs. Also, the data structures are generally not well-suited for theorem proving. I'd like to go back and rewrite some parts so that they would be useful for theorem proving and more "compatible" with mathlib in general.
Based on some of the links listed here I guess I should work on providing a Prop of the form ts |= e where ts is some transition system and e is some LTL/CTL expression. Also I know that mathlib4 has several sections concerning graphs and DFA/NFA so would it be useful to make my transition system representation compatible/isomorphic with those?

[Karl Palmskog]

for CTL and friends, state of the art in Coq is this: https://github.com/coq-community/comp-dec-modal

[Ira Fesefeldt]

I'd agree that a Prop that looks something like ts |= e could be useful. Furthermore, you could maybe than prove soundness theorem that says ts |= e iff algo(ts,e)=true. However, I am not sure how to connect it to mathlib. DFAs\NFAs are afaik not isomorphic to transition systems due to FAs having a certain accepting condition. LTL Model Checking uses Büchi accepting criterias instead of FAs accepting criterias anyway.

[Ira Fesefeldt]

From just looking around, I saw that mathlib offers methods for computing the transition system of a turing machine. Maybe this could be something to look into?

[Andrés Goens]

Ira Fesefeldt said:

I'd agree that a Prop that looks something like ts |= e could be useful. Furthermore, you could maybe than prove soundness theorem that says ts |= e iff algo(ts,e)=true. However, I am not sure how to connect it to mathlib. DFAs\NFAs are afaik not isomorphic to transition systems due to FAs having a certain accepting condition. LTL Model Checking uses Büchi accepting criterias instead of FAs accepting criterias anyway.

but you can transform them to equivalent transition systems/kripke structures, can't you? Where for every accepting state in an NFA/DFA you just have a transition to itself

[Ira Fesefeldt]

Andrés Goens said:

but you can transform them to equivalent transition systems/kripke structures, can't you? Where for every accepting state in an NFA/DFA you just have a transition to itself

I am not sure that this is always the transition system you actually would like to have? Alternatively, one could consider the transition system where instead of a self-loop, there is a transition from accepting states to some sink state? Or even another alternative, you could only label accepting states with a label accept? I would claim that it is not trivial, on which transformation from FA to transition system you would like to do model checking.

[Shreyas Srinivas]

Ira Fesefeldt said:

I'd agree that a Prop that looks something like ts |= e could be useful. Furthermore, you could maybe than prove soundness theorem that says ts |= e iff algo(ts,e)=true. However, I am not sure how to connect it to mathlib. DFAs\NFAs are afaik not isomorphic to transition systems due to FAs having a certain accepting condition. LTL Model Checking uses Büchi accepting criterias instead of FAs accepting criterias anyway.

I think changing this is not difficult. For DFAs, the terminating condition is being in a set (i.e. satisfying some property), instead we replace this with some property suitable for Buchi automaton. There must be some way to express that some state occurs infinitely in an accepting run.

[Shreyas Srinivas]

Where I got stuck in my naive attempt was that there was no explicit way to do transfinite induction.

[Gary Haussmann]

If the transition system is a directed graph then the Buchi criteria could be that a (reachable) cycle exists containing the accepting set.
If I want to create/use theorems regarding model checking I think both the transition system and the temporal logic expressions need to be of a form that Lean tactics can easily manipulate.