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 [http://is.ifmo.ru/books/_principles_of_model_checking.pdf 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 [http://is.ifmo.ru/books/_principles_of_model_checking.pdf 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 [http://is.ifmo.ru/books/_principles_of_model_checking.pdf 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!!