Automated Verification: Assignment 6

1. Show that PLTL with the Next and Until operators is more expressive that PLTL with the Next and Always operators.
2. Show that the property "p holds only in even positions" is not expressible in PLTL.
3. Consider PLTL extended with past operators (since, previous, and weak previous). Describe (without a proof) the construction of the automaton A_phi that accepts precisely models(phi).
4. Show that alternating automata on finite words (AFW) are closed with linear blow-up under intersection, disjunction, and negation.
5. Consider a projection h from an alphabet Sigma to an alphabet Delta. Provide an example for the failure of the "straightforward" closure of AFW under projection in which we define the transition rho^h(s,b) as the disjunction of rho(s,a) for all a in Sigma such that h(a)=b.
6. Show that every node in an accepting run of an ABW has a well-defined rank (use Königs' Lemma). Use this to show that if an ABW accepts an infinite word than it has a memoryless accepting run on this word.