Automated Verification: Assignment 4

1. Prove by induction on the structure of formulas that every PLTL formula f can be translated to a Büchi automaton A_f such that the language of A_f is precisely models(f).
2. Prove by induction on the structure of formulas that an infinite word over 2^cl(f) is a Hintikka sequence for a computation sigma and a PLTL formula f iff it is a satisfaction sequence for sigma and f.