CURRENT TEACHING
  • Algorithms for Model Checking (2IMF35), Q3, 2015-2016.
    Treats the mu-calculus and CTL* and its subsets LTL and CTL, and various approaches and algorithms for verifying formulae in these logics. These include the standard labelling algorithms and the symbolic (fixed point based) algorithms for CTL, and fair CTL. The Emerson-Lei algorithm for verifying the mu-calculus is analysed and discussed. Transformations of the model checking problem to the frameworks of Boolean equation systems and Parity Games are addressed, combined with advanced algorithms for solving the latter artefacts.