1. Given the following propositional logic formula

pre(X) = {s | P ath(s).[1] X} and h1,2 (X) = [[2]] ([[1]] pre(X))

where is are CTL properties and [[]] denotes the propositional logic formulas representing the semantics of . Assuming the definition of pre as discussed in class.

Compute the least fixed point of the functions h pq,false, hfalse,pq , hpq,q and hpq, pq on the following Kripke structure M = (S, T, L) where

S = {s0, s1, s2, s3}

T = {(s0, s1),(s1, s2),(s1, s3),(s2, s1),(s3, s2)}

p L(s0) L(s2) L(s3), q L(s2), q L(s3)

Show the steps of your computation.