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

**URL:** <https://forum.anoma.net/t/model-checking-from-the-origins-to-perfomance-evaluation-or-at-least-some-of-it/470>\
**Category:** Education\
**Created:** [February 6, 2024, 4:34pm UTC](https://forum.anoma.net/t/model-checking-from-the-origins-to-perfomance-evaluation-or-at-least-some-of-it/470 "2024-02-06T16:34:48Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![graphomath](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/graphomath/32/9_2.png) [@graphomath](https://forum.anoma.net/u/graphomath)\
**Post date:** [February 6, 2024, 4:34pm UTC](https://forum.anoma.net/t/model-checking-from-the-origins-to-perfomance-evaluation-or-at-least-some-of-it/470/1 "2024-02-06T16:34:48Z")

</div>

[Model Checking](https://en.wikipedia.org/wiki/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](https://en.wikipedia.org/wiki/Linear_temporal_logic), [CTL](https://en.wikipedia.org/wiki/Computation_tree_logic), 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](https://en.wikipedia.org/wiki/Principles_of_Model_Checking)

Roughly, I propose that we go through these courses:

- [Model Checking | Informatik 2](https://moves.rwth-aachen.de/teaching/ss-23/model-checking/)
- [Modelling and Verification of Probabilistic Systems | Informatik 2](https://moves.rwth-aachen.de/teaching/ws-23-24/modelling-and-verification-of-probabilistic-systems/)

However, any thoughts are welcome.

---

<div class="post-metadata">

**Author:** ![graphomath](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/graphomath/32/9_2.png) [@graphomath](https://forum.anoma.net/u/graphomath)\
**Post date:** [February 16, 2024, 4:34pm UTC](https://forum.anoma.net/t/model-checking-from-the-origins-to-perfomance-evaluation-or-at-least-some-of-it/470/2 "2024-02-16T16:34:07Z")

</div>

Some resources:

- [The Probabilistic Model Checking Landscape](https://moves.rwth-aachen.de/wp-content/uploads/lics2016_tutorial_katoen.pdf)
- [TOOLympics 2019](https://www.sosy-lab.org/research/pub/2019-TACAS.TOOLympics_2019_An_Overview_of_Competitions_in_Formal_Methods.pdf)
- [TOOLympics 2023](https://tacas.info/toolympics2023.php) also featuring informal system’s Aᴘᴀʟᴀᴄʜᴇ
- [In the quantitative automata zoo](https://www.sciencedirect.com/science/article/pii/S0167642315002580)  
 ![image](https://europe1.discourse-cdn.com/flex013/uploads/anoma1/original/1X/483c790b70e55e66043cadb7c09e58a7670e2644.png)  
 ![image](https://europe1.discourse-cdn.com/flex013/uploads/anoma1/original/1X/cd91bea3af7548a2b0a350038c5efaefa007f089.png)  
-[Tutorial: Probabilistic Model Checking](https://resources.mpi-inf.mpg.de/departments/rg1/conferences/vtsa17/slides/baier-vsta17-MC-final.pdf)  
-[**The Book** Principles of Model Checking](https://www.researchgate.net/publication/220690719_Principles_of_Model_Checking) [_(errata)_](https://i2docker.moves.rwth-aachen.de/i2/fileadmin/user_upload/documents/Introduction_to_Model_Checking/errata.pdf)

---

<div class="post-metadata">

**Author:** ![graphomath](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/graphomath/32/9_2.png) [@graphomath](https://forum.anoma.net/u/graphomath)\
**Post date:** [February 23, 2024, 11:02am UTC](https://forum.anoma.net/t/model-checking-from-the-origins-to-perfomance-evaluation-or-at-least-some-of-it/470/3 "2024-02-23T11:02:14Z")

</div>

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](https://www.sciencedirect.com/science/article/pii/S0168007205000886#).

There is an interesting extension of the usual temporal logics: [Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications](https://www.researchgate.net/publication/220298303_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.