Datastructures & Algorithms for Modelchecking
State Space Representations & Explorations

Dat5/F9D, Fall 2001

1 Overview

In this Dat5/F9D course we cover a mixture of classical and emerging techniques from the area of modelchecking, such as

• Linear Temporal Logic & Büchi Automata.
• Partial Order Reduction  & Symmetri Reduction.
• Probabilistic Models & Logics (Markov Chains, Markov Decision Processes, PCTL, MTBDDs).
• (Quantified) Propositional Logic, BDDs, BEDs, SAT-solvers.
• Bounded & Directed Model Checking.
• Compositionality, Abstraction, Acceleration.
• Automata Representations.
• Games and Gameautomata.
• Infinite State Models.
• Distributed Modelchecking.

 

The course will consider various (extended) models and logics for expressing behaviour and behavioural propertis.  Emphasis will be on datastructures and algorithms suggested for representing and exploring the (large or even infinite) state-spaces described by the models. The literature is quite preliminary and is still under development.   Part of the course will consist of student presentation (a total of 16) and additional presentations by myself (Kim G Larsen) and possible guest presenters. A high degree of interaction and frequent discussions will be encouraged.It is expected that you attend all sessions, read (and mostly understand) the papers for each session, and are able to pose "nasty" questions to the presenters about the papers. Note that it may in some cases, e.g., when presenting a paper yourself, be necessary to read additional papers referenced by your paper in order to fully understand your own paper.

Suggested literature (under the above given themes) can be found here.

2 Schedule

Lectures (and exercises) are scheduled Tuesdays 9:00 - 12:00, generally in E3-209 (see the schedule). The schedule is at present only partial but will be completed during the course (thus, carefully observe the web-page).

 

When	Who	What
TU, Sep 4	KGL	Introduction of DAT5  LTL and Büchi Automata; JPK chapter 2.
TU, Sep 11	KGL	LTL and Büchi Automata Partial Order Reduction; CGP sections 11.1-11.4 (CGP omhandler Büchi Automater).
TU, Sep 18	Anders	S. Bensalem, Y Lakhnech and S. Owre: Computing Abstractions of Infinite State Systems Compositionally and Automatically
TU, Sep 25	Daniel    KGL	Chapters 1-3 in Dennis Dams: Abstract Interpretation and Partition Refinement for Model Checking Markov Chains & Decision Processes; Probabilistic Bisimulation; Probabilistic Temporal Logics.    Lit.:  Jonsson, Larsen, Yi: Handbook (ch.1,2,3,5)            Hansson, Jonsson: A Framework for Reasoning                                about Time  and Reliability.
THU, Sep 27 10:00-13:00	Anders Jakob	Symbolic Model Checking for Probabilistic Processes. On the Representation of Probabilities over Structured Domains . [Abstract and Postscript]
TU, Oct 9		Marta Kwiatkowska: PRISM and related topics. Bertrand, Henrik, Kim:   Probabilistic Verification using Refinements.
TU, Oct 16	Jacob Jens	Probabilistic Extensions of Process Algebras . Bengt Jonsson, Kim G. Larsen and Wang Yi Symbolic Model Checking of Concurrent Probabilistic Systems Using MTBDDs and Simplex. Marta Kwiatkowska, G. Norman, D. Parker and R. Segala
TU, Oct 23	Ulrik John Kim	Verification of Large State/Event Systems using Compositionality and Dependency Analysis :   Jørn Lind-Nielsen, Henrik Reif Andersen, Gerd Behrmann, Henrik Hulgaard, Kåre Kristoffersen, Kim G. Larsen Kim G. Larsen, Arne Skou:  Bisimulation through Probabilistic Testing Stanley N. Burris  Logic for mathematics and computer science  Prentice Hal (afsnit 2.10 og evt 2.9 og 2.11) fås hos Hanne Frøde Uribe, Stickel:   Ordered Binary Decision Diagrams and the Davis-Putnam  Procedure.
THU, Nov  1	Alle	Mary Sheeran, Gunnar Stålmarck: A tutorial paper on Stålmarck's method of proof for propositional logic
TU, Nov 13	Ulrik Jens Jacob	Symbolic Reachability Analysis based on SAT-Solvers , Parosh A. Abdulla, Per Bjesse, Niklas Eén, TACAS'00 (best paper award at TACAS'00). Mary Sheeran, Satnam Singh: Checking safety properties using induction and a SAT-solver.
TU, Nov 20	Jens Anders Frehse	Generating BDDs for Symbolic Model Checking in CCS, Enders, Filkorn, Taubner . (se mappen). (kl 10:00) "Boolean Expression Diagrams" by Henrik Reif Andersen and Henrik Hulgaard . Appears in the proceedings for LICS '97 . Available as PostScript (gzip'ed) , PostScript , and PDF . Assume-Guarantee Verification of Timed Systems (kl 13:00)
TU, Nov 27	XX YY
WE, Nov 28	NN MM
TU, Dec 11		Præsentation af projekter

3 Material & Links

• [JPK] Joost-Pieter Katoen: " Concepts, Algorithms, and Tools for Model Checking" . (Lecture Notes)
• [CPG] Clarke, Grumberg, Peled: Model Checking.
• SPIN homepage .
• MUPHI homepage .
• Ed Clarke's homepage .
• Doron Peled's homepage .
• Moshe Vardi's homepage .
• SAT-live homepage .
• Fabio Somenzi homepage
• Marta Kwaitkowska homepage .
• Joost-Pieter Katoen homepage .
• Holger Hermanns homepage .
• John Hatclif homepage .
• Rajeev Alur homepage .
• Tom Henzinger homepage .

5 Presentation Hints (points to be discussed)

The following is a list of hints for making more effective presentations. Note that the hints are not firm rules and should be adapted to the specific situation in which they are used. We will restructure and update the list during the course.

• Make sure that the presentation has a simple structure and that the listener understands and is able to follow the structure during the presentation. There should probably be an overview slide at the beginning and a talk summary/conclusions slide at the end. It may be useful to remind the listener of the structure during the presentation.
• It is often a good idea to divide a presentation into three separate parts. The first part should present the material without criticism, but be as faithfully to the authors as possible. The second part then relates the material to a) related work, e.g., as presented on DAT5 and b) your DAT5 project. The third part evaluates both form and content of the presented material, i.e., good and bad points. A self-evaluation of the presentation is also possible (not done at the exam). The time spent on these parts should be about 20, 5, and 5 minutes, respectively (give or take a few minutes), as this follows the DAT5 exam format.
• It is generally a good idea to mix general observations with concrete examples. It is often time-consuming and difficult to construct good, specific examples, but the time spent on this is well spent. Important observations that the listener should definitely understand are prime candidates for exemplification.
• Rehearse the presentation in front of an audience before the exam. It is important to actually say out loud all words of the presentation. Only this way is it possible to get a good feeling for the length of the talk and to identify trouble spots in the presenation that need further work.
• Make sure that the slides are easy to present. If some transitions between slides are difficult to remember then the slides should probably be revised. Again, the way to identify problems is through saying all the words out loud.
• Do number the slides; this makes it easier for the listeners to later refer to them.
• For the exam, it is a good idea to have everything on the slides so that there is no need to draw spontaneous pictures on the board.

Kim G. Larsen (kgl@cs.auc.dk)