Question 3) Consider the following transition system depicted in Figure 1, with all the states, transitions and state variables. There are four propositional variables p, q, r and s. All of them are false in the initial state s0, p and s are true in the state si, q is true in the state s2, and rare true in the state s3, and so on. Express the following properties in CTL and state whether they hold in the transition system. If a property does not hold then show a counter example. (i) Always, in the next state q is false. (5 marks) (ii) There is a possibility that the system never reach a state where r is true (5 marks) (5 marks) (iii) Always, r is false until a is true s1 (p.s) (p,q,s) 54 {9) (p, q) s5 s2 50 {9,r) (p,q,r) s3 56 Figure 1. An example transition system