Objectives:

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

**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):

- $(E_1 + E_2).F^\omega \equiv E_1.F^\omega + E_2.F^\omega$
- $E.(F_1 + F_2)^\omega \equiv E.F_1^\omega + E.F_2^\omega$
- $E.(F.F^*)^\omega \equiv E.F^\omega$
- $(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!!