Friday, February 25, 2005

mu-calculus and CTL

Introduction to translation from CTL to modal mu-calculus.

Tuesday, February 15, 2005

Assignment 1 released

The assignments page has the details.
Now with the corrected link!
Deadline changed - now 2400 4th March 2005!

Friday, February 11, 2005


NuSMV is a symbolic model checker. NuSMV2, combines BDD-based model checking and SAT-based model checking.

Tuesday, February 08, 2005

Temporal Logic: CTL

Friday, February 04, 2005

Finite State Machines

Tuesday, February 01, 2005

STRIPS planning

Recap of SAT and phase transition Zhang slides part 1 pp. 26-36.


  • PropPlan
  • Actions, preconditions postconditions.
  • Frame problem
  • Logical formulation using quantified boolean formula (QBF)