Model-Checking SS 2014

News | Basic information | Content | Exercises | Slides | Links

Lectures are accompanied by a weekly exercise lesson.

Exercise Sheets

• 11 Apr. 2014 : Exercise sheet #1 [PDF] Note that you are expected to download and install Spin Some useful links: Getting started Spin Manual Promela documentation
• 18 Apr. 2014 : Good Friday (no exercise session)
• 25 Apr. 2014 : Exercise sheet #2 [PDF] prepare exercises 2.1 and 2.2
• 2 May 2014 : Exercise sheet #3 [PDF] Exercise 3 is the difficult one
• 9 May 2014
• 16 May 2014 : Exercise sheet #4 [PDF]
• 23 May 2014
• 30 May 2014 : Exercise sheet #5 [PDF]
  Around the LTL to Büchi transformation, we will detail what tricks we can use. Build a Büchi automaton over alphabet $\{a,b,c\}$ accepting each of the following LTL formulas:
  • $ a \,\mathcal{U}\, ( b \,\mathcal{U}\, c ) $
  • $ (a \,\mathcal{U}\, b )\,\mathcal{U}\, c $
  • $ \mathbf{G}\, (a \to ( (a \vee b) \,\mathcal{U}\, c)) $
• 6 Jun. 2014: Exercise sheet #5.1 [PDF] (instead of #5)
• 13 Jun. 2014 : Lecture instead
• 20 Jun. 2014: Exercise sheet #6 [PDF] We will show that $E\mathbf{X}, E\mathbf{G}$ and $E\,\mathcal{U}$ are enough to define any other CTL operator. Then we will consider the composition of some unary CTL operators, noticeably $E\mathbf{F}A\mathbf{F}$ and $A\mathbf{F}E\mathbf{F}$. Finally we will perform some computation of fixpoints, to determine for instance how to compute states satisfying $A\mathbf{G}A\mathbf{F}\,p$.
• 27 Jun. 2014 : Lecture instead
• 30 Jun. 2014 : No exercise sheet, maybe a solution Finishing exercise sheet #6 and building BDDs for some boolean formulas (4 variables), building conjunctions of bdd's, and perhaps eventually existential projection over bdd's
• 4 Jul. 2014 : Lecture instead
• 7 Jul. 2014: Exercise sheet #7 [PDF] A little bit more on BDD's and some exercises about abstraction
• 8 Jul. 2014: Last session Building the Büchi translation of $\mathbf{G}(((\mathbf{X}p)\,\mathcal{U}\,q)\to (p\vee q))$ and finishing exercise sheet #7.
• 11 Jul. 2014 : Exam Solution of Exercise 2: The negation of the property was $\mathbf{EF}\,(p\wedge ((p\vee q) \,\mathbf{E}\mathcal{U}\, q))$. The property could therefore be expressed by the formula $\mathbf{AG}(p\to \neg ((p\vee q)\,\mathbf{E}\mathcal{U} \,q))$.