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!!

cs-486/homework-4.txt · Last modified: 2017/02/08 16:26 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0