Automated Verification: Assignment 5

1. Prove that the automaton A^H_phi accepts an infinite word (a₀,Q₀),(a₁,Q₁),... precisely when Q₀,Q₁,... is a Hintikka sequence for a₀,a₁,... and phi. Use this to show that A_phi accepts precisely models(phi).
2. Show that for each n there is a PLTL formula of length O(n) such that if A is a Büchi automaton that accepts precisely models(phi), then A has at least 2ⁿ states.
3. Prove by reduction from the space-bounded tiling problem that satisfiabilty, validity, and model checking for PLTL are PSPACE-hard.
4. Let A=(Sigma,S,s₀,rho,F) be an alternating automaton. Let A'=(Sigma,2^S,{{s₀}},rho',2^F) be a nondeterministic automaton where rho'(T,A)={T' : T' satisfies rho(t,a) for all t in T}. Show that L(A)=L(A').