### mu-calculus and CTL

Introduction to translation from CTL to modal mu-calculus.

Course Lecture Log, MSc Informatics, The University of Edinburgh, Spring 2005.

The assignments page has the details.

Now with the corrected link!

Deadline changed - now 2400 4th March 2005!

Now with the corrected link!

Deadline changed - now 2400 4th March 2005!

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

- User Manual
- Tutorial
- Foils
- A copy of the NuSMV binary is available on DICE at /home/mfourman/bin/NuSMV

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)