Model Checking μ-Calculus and CTL -- Examples from Previous Exams

This page contains a list of exercises about model checking of previous exams. By pressing the check button, the Kripke structure is drawn and the listed formulas are checked. The tool behind is the same model checker as used in the online tool.

Exam of 2013, October 7; Problem 7

Exam of 2013, July 22; Problem 7

Exam of 2012, March 19; Problem 4 (first part)

Exam of 2012, March 19; Problem 4 (second part)

Exam of 2012, February 13; Problem 5

Exam of 2010, December 8; Problem 5

Exam of 2010, September 23; Problem 7

Exam of 2010, July 23; Problem 4