Notes on the MCCourse, 2019

course 1

Need to review slide 42–44, missing discussion on the access order of locks adding explicitly the example of the DEC computer.

finished the 1st course after the swimming pool exercise, just before the SCC part.

I Should separate the part on product of automata and tell more about its use for \cap and product of languages (+ maybe deterministic vs not) and have a dedicated section on product of nets and use for compositional reasonning.

course 2

took 1 hour to study SCC and the examples. Did most of the exercise. Not enough time to do printer queue.

discussion on arc extension is too vague, need to add material on decidability ; same regarding the product; need a better explanation of why it is interesting.

course 3

Plan to spend most of it on examples.

Started course MCC-3 about user-defined property, up until 23.

Need to illustrate the difference between specification and implementation and the use of properties as a way to specify the system.

There is a bug in the product of slide 18.

Actually, there is a need to explain product of automaton for doing inclusion in course MCC-1 better. Slide 17 on using Petri instead of automaton is a bad idea.

Add examples of Büchi automata which have an empty language even though they are not trivial.

course 4

Most of them did not work on tp3 and therefore were not able to experiment with selt on the resourece+client example. I should make sure that they all can use tina.

course 5

spent 1/2 hour on reviewing answers to TP2; still a good exercise. Then started working on TP4 + reviewing LTL formulas. LAst hour dedicated to MCC_4 (Karp-Miller)

course 6

2 slots for exam.

course 7

write somewhere that Bryant paper is the most cited in CS. Add example of model-checking with BDD

next year I should add SAT-based BMC methods + new exercises

course 8

add use of the BDD interface http://formal.cs.utah.edu:8080/pbl/BDD.php

good example using Mickey net to show we can compute reachable markings in 1 iteration; add another example that is more credible

It is possible to add things to the course for the same kind of audience, say Tarski + fixpoints, then how to model-check CTL using fixpoints and Muse kind of logic, then BDD style.

Should find a better way to generate questions and feedback from the audience and force them to model durng class, e.g. sprints for giving results.