Objectives:

• Practice creating verification models with PROMELA
• Learn Buchi Automata semantics
• Write omega-regular expressions

## Problems

1. (16 points) This problem is Exercise 4.7 in Principles of Model Checking. Prove or disprove the following equivalences for $\omega$-regular expressions (the .-operator is concatenation):

1. $(E_1 + E_2).F^\omega \equiv E_1.F^\omega + E_2.F^\omega$
2. $E.(F_1 + F_2)^\omega \equiv E.F_1^\omega + E.F_2^\omega$
3. $E.(F.F^*)^\omega \equiv E.F^\omega$
4. $(E^*.F)^\omega \equiv E^*.F^\omega$

2. (10 points) This problem is Exercise 4.9 in Principles of Model Checking. Let $\Sigma = \{A,B\}$. Construct an NBA that accepts the set of infinite words $\sigma$ over $\Sigma$ such that $A$ occurs infinitely many times in $\sigma$ and between any two successive $A$'s an odd number of $B$'s occur.

3. (10 points) This problem is Exercise 4.11 in Principles of Model Checking. Give an NBA for the $\omega$-regular expression $(AB + C)^*((AA+B)C)^\omega + (A^*C)^\omega$

4. Finish up any previous homework!!