Automated Verification: Assignment 7

1. Define a temporal connective W with the property that ~(f U g) is equivalent to (~g) W (~f). Define the alternating transition rho(f W g,a).
2. Show that an alternating Büchi automaton (ABW) has an accepting run iff it has a run in which infinitely many levels have finite rank.
3. Show that an alternating Büchi automaton has an accepting tree run iff it has an accepting dag run.
4. Prove the correctness of the Miyano-Hayashi translation of ABW to NBW. That is, show that the nondeterministic Büchi automaton Aⁿ that was constructed from the alternating Büchi automaton A accepts the same infinitary language as A.
5. Construct directly a nondeterministic Büchi automaton for the formula (p U q) U r. Compare it to the nondeterministic automaton that you will get, using the Miyano-Hayashi translation, from the alternating Büchi automaton defined in class for this formula.