 After successful completion of the course, participants are able to: recognize situations in which the applications of model checking techniques for specification and analysis may be useful,
 explain the basic theory and algorithms of model checking for finite state, realtime, and probabilistic automata,
 model (critical parts of) realistic computerbased systems as networks of automata,
 formalize desired properties of these systems in terms of automata or temporal logic, and
 use stateoftheart tools for their analysis.

 As our daily lives depend increasingly on digital systems, the reliability of these systems becomes a crucial concern, and as the complexity of the systems grows, their reliability can no longer be sufficiently controlled by traditional approaches of testing and simulation. It becomes essential to build mathematical models of these systems, and to use (algorithmic) verification methods to analyse these models. In model checking, specifications about the system are expressed as (temporal) logic formulas, and efficient symbolic algorithms are used to traverse the model defined by the system and check if the specification holds or not. As model checking is fully automatic, requiring no complex knowledge of proof strategies or biases of simulation tools, it is the method of choice for industryscale verification. This course introduces several variants of model checking, in particular:  Explicitstate and symbolic algorithms for model checking lineartime (LTL) and branchingtime (CTL) temporal logics for finite machines
 DBMbased algorithms for model checking TCTL for networks of timed automata
 PCTL for Markov chains and Markov decision processes
 Statistical model checking





Depending on the interest of the students, requirements imposed by homework assignments, and recent scientific developments, the specific topics covered in this course may vary slightly from year to year. 
linear time temporal logic (LTL); branching time temporal logic (CTL); explicitstate model checking; bounded model checking; timed automata, DBMs; probabilistic CTL; Markov chains and Markov decision processes; statistical model checking; model checking tools such as nuSMV, Uppaal, MRMC, Uppaal SMC and PRISM. 
Grades will be awarded on the basis of an exam and three larger homework assignments. In computing the final score, the exam counts equally heavy as the three assignments combined. 
Some knowledge of automata theory; probability theory; computational complexity. 
Most of the theory discussed in the course is presented in the textbook Principles of model checking / Christel Baier; JoostPieter Katoen. – Cambridge, Mass: MIT Press, 2008. This book is strongly recommended. The remaining course material consists of handouts, sheets, and recent papers from the literature. These will be made available electronically via the course webpage or distributed during the course. 
• 32 hours lecture • 60 hours group project work without guidance • 32 hours problem session • 44 hours individual study period Extra information teaching methods: Lectures, practicals and homework assignments. 
  Verplicht materiaalHandoutsHandouts, sheets, and recent papers from the literature. 

 Aanbevolen materiaalBoekMost of the theory discussed in the course is presented in the textbook Principles of model checking / Christel Baier; JoostPieter Katoen. – Cambridge, Mass: MIT Press, 2008. This book is strongly recommended. 

 WerkvormenCursus AlgemeenLectures, practicals and homework assignments.
 Hoorcollege
 Project
 Werkcollege
 Zelfstudie

 ToetsenTentamenWeging   1 
Gelegenheden   Blok KW4, Blok KW4 


 