**This is an old revision of the document!**

Objectives:

• Implement EU and EG using fix-points.
• Do symbolic CTL model checking.

## Problems

1. (40 points) Write algorithms to compute EG and EU as fix-point calculations using either the Cudd or your library from Homework 12. Include tests that automatically check the correctness of your implementation. 20 points are allocated to the algorithms and the other 20 points are allocated to the quality of the tests.

2. (40 points) Verify the Hyman's Mutual Exclusion protocol below for two threads using the EG and EU code from the first problem. Check for mutual exclusion and fairness (e.g., a thread requesting the critical section infinitely often gets the critical section infinitely often).

Hyman's Mutual Exclusion

void lock (int i) {
int j = 1 - i;
signal[i] = 1;
while (turn != i) {
while (signal[j]);
turn = i;
}
}

void unlock(int i) {
signal[i] = 0;
}

3. (40 points) Verify the Peterson's mutual exclusion protocol below for two threads using the EG and EU code from the first problem. Check for mutual exclusion and fairness (e.g., a thread requesting the critical section infinitely often gets the critical section infinitely often).

Peterson's Mutual Exclusion

void lock (int i) {
int j = 1 - i;
signal[i] = 1;
turn = j;
while (signal[j] && turn != i);
}

void unlock(int i) {
signal[i] = 0;
}