Model Checking: from the origins to perfomance evaluation or at least some of it

Education
1

Model Checking has been mentioned at several occasions in meetings, slack conversations, and forum posts. It is a method that often promises fully automatic verification of systems, i.e., that a system has all the desired properties. Although the “fully automatic” in that sentence is usually a bit of a stretch, model checking is known for catching errors. For sure, you can play with it! I would even go as far and say that it is easier to play around with than any of Coq, Agda, Lean, etc., but maybe dependent types and programming in Lean is your cup of tea.

Now and here, I just bluntly claim that we all need to speak the specification languages of model checking, i.e., the languages that are used to describe system properties, in particular LTL, CTL, and in particular understand the general notion of liveness and safety properties. There’s a “the book” on the topic: Principles of Model Checking - Wikipedia

Roughly, I propose that we go through these courses:

However, any thoughts are welcome.

2

Some resources:

3

All these models come with a list of logics that have been proposed to reason about the behavior of the models. One “dream property” is the Henessy Milner property.

There is an interesting extension of the usual temporal logics: Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications. This might be yet another route to get into game theory from distributed systems.