1. (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.
2. (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.

Use the CUDD package for the following problems.

1. (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.