    Course module   NWIIMC046  Category   MA (Master)  Language of instruction   English  Offered by   Radboud University; Faculty of Science; Informatica en Informatiekunde;  Lecturer(s)     Academic year   2020   Period   KW3KW4  (25/01/2021 to 31/08/2021) 
 Starting block   KW3  
 Course mode   fulltime  
 Remarks     Registration using OSIRIS   Yes  Course open to students from other faculties   Yes  Preregistration   No  Waiting list   No  Placement procedure    
      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, and techniques and tools in particular:
 Explicitstate and symbolic algorithms for model checking lineartime (LTL) and branchingtime (CTL) temporal logics for finite machines
 Symbolic model checking using BDDs
 Bisimulation abstraction techniques
 Model checking in machine learning applications
 PCTL for Markov chains and Markov decision processes
 Abstraction techniques for probabilistic model checking
 Counterexamples for probabilistic model checking
 Model checking tools (NuSMV and PRISM)
 Applications of model checking for analysis of distributed algorithms and for faulttree analysis
Instructional Modes
 Lecture
 Tutorial
 Selfstudy


  Some knowledge of automata theory; probability theory; computational complexity. 
 Grades will be awarded on the basis of an exam and homework assignments. 
 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. 



   Required materialsHandoutsHandouts, sheets, and recent papers from the literature. 
 BookMost 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 mandatory. 
ISBN  :   9780262026499 


Instructional modesCourse GeneralLectures, practicals and homework assignments.
 Project

 TestsFinal examTest weight   1 
Test type   Exam 
Opportunities   Block KW4, Block KW4 
RemarkThe midterm is optional. Students may also do the full exam at the end of the course. There is no separate resit .
 AssignmentsTest weight   1 
Test type   Assignment 
Opportunities   Block KW4 
 Midterm examTest weight   0 
Test type   Exam 
Opportunities   Block KW3, Block KW4 


  
 
 