This homework is to practice using BDDs for symbolic model checking.

## Paper Pencil

(

**3 points**) Write a CTL property for the transition relation for the dinning philosophers system in

Homework 3–the property must require a least or greatest fix-point to compute.

(**5 points**) At an abstract level, similar to what we did on the board in lecture, perform symbolic model checking for the formula in the prior problem. Be sure to show each step of the fix-pont computation. Please note that if the **when** clause is correctly treated as a single atomic action (i.e., the test, state update, and goto are one step), then there are only 10 reachable states.

## Programming

Use the CUDD package for the following problems.

(

**10 points**) Write a program in CUDD using your solution from

Homework 6 that does symbolic model checking for your formula in the prior problem.

Back to top