mu-calculus and CTL

Introduction to translation from CTL to modal mu-calculus.

Assignment 1 released

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

NuSMV

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

Temporal Logic: CTL

Stuttgart CTL Notes

Finite State Machines

STRIPS planning

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

STRIPS

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