3. This questions concerns the foundations of model checking. For Parts (a) and (b) consider the following Bchi automaton over the alphabet {a, b}. a, b 3 a b a a b 2 a (a) Give an w-word that is accepted by the Bchi automaton above. Justify your answer. [4 marks] (b) Give an w-word that is not accepted by the Bchi automaton above. Justify your answer. [3 marks] [6 marks] (c) Give a Bchi automaton accepting exactly the models of the LTL formula (p^OO p). Argue informally why your answer is correct. (d) Give a Bchi automaton accepting exactly the models of the LTL formula (p) ^ (09). Argue informally why your answer is correct. [7 marks]