NWI-IMC046
Model Checking
Course infoSchedule
Course moduleNWI-IMC046
Credits (ECTS)6
CategoryMA (Master)
Language of instructionEnglish
Offered byRadboud University; Faculty of Science; Informatica en Informatiekunde;
Lecturer(s)
PreviousNext 1
Coordinator
dr. N.H. Jansen
Other course modules lecturer
Examiner
dr. N.H. Jansen
Other course modules lecturer
Lecturer
dr. N.H. Jansen
Other course modules lecturer
Contactperson for the course
dr. N.H. Jansen
Other course modules lecturer
Lecturer
prof. dr. M.I.A. Stoelinga
Other course modules lecturer
Academic year2020
Period
KW3-KW4  (25/01/2021 to 31/08/2021)
Starting block
KW3
Course mode
full-time
Remarks-
Registration using OSIRISYes
Course open to students from other facultiesYes
Pre-registrationNo
Waiting listNo
Placement procedure-
Aims
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, real-time, and probabilistic automata,
  • model (critical parts of) realistic computer-based systems as networks of automata,
  • formalize desired properties of these systems in terms of automata or temporal logic, and
  • use state-of-the-art tools for their analysis.
Content
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 industry-scale verification.
This course introduces several variants of model checking, and techniques and tools in particular:
  • Explicit-state and symbolic algorithms for model checking linear-time (LTL) and branching-time (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 fault-tree analysis
Instructional Modes
  • Lecture
  • Tutorial
  • Self-study
Level

Presumed foreknowledge
Some knowledge of automata theory; probability theory; computational complexity.
Test information
Grades will be awarded on the basis of an exam and homework assignments.
Specifics
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 materials
Handouts
Hand-outs, sheets, and recent papers from the literature.
Book
Most of the theory discussed in the course is presented in the textbook Principles of model checking / Christel Baier; Joost-Pieter Katoen. – Cambridge, Mass: MIT Press, 2008. This book is mandatory.
ISBN:9780262026499

Instructional modes
Course

General
Lectures, practicals and homework assignments.

Project

Tests
Final exam
Test weight1
Test typeExam
OpportunitiesBlock KW4, Block KW4

Remark
The midterm is optional. Students may also do the full exam at the end of the course. There is no separate resit .

Assignments
Test weight1
Test typeAssignment
OpportunitiesBlock KW4

Midterm exam
Test weight0
Test typeExam
OpportunitiesBlock KW3, Block KW4