ASSIGNMENT 9 - FORMAL MODELS EXERCISES, SUMMER 2011


Selected Solutions to Exercise 35:


Formula 4: E [<x>1 U <z>1] holds in all states 0, 1, 2 and 3.

E.g. it holds in state 0 because: we have to find at least one path
starting in state 0 (i.e. the "E" quantifier) such that subformula
[<x>1 U <z>1] holds on that path. Let P = 0,3,... be that
path. Following the semantics of "U", subformula [<x>1 U <z>1]
requires that we find at least one state s' along P sucht that <z>1
holds in s'. Once we have such state s', additionally <x>1 must hold
on all states which are predecessors of s' in P. Note that <x>1 does
not have to hold in state s' (although it could). We select s' to be
the first state of P, i.e. s' = 0. Then <z>1 holds in s'. Since s'
does not have any predecessors in P, the additional requirement of
<x>1 is vacuously satisfied. Therefore, E [<x>1 U <z>1] holds in state
0.

Checking states 1, 2, 3 is similar, e.g. formula 4 holds in state 3
because: let path P = 3,2,0... Then <z>1 holds in state s' = 0, and
additionally <x>1 holds in all predecessors of s', i.e. in states 2
and 3. Note that checking <x>1 is independent of the transitions in
path P, i.e. it does not matter that there is a transition from 3 to 2
with symbol 'y' in P.


Formula 6: EF (EG <x>1) holds in all states 0, 1, 2 and 3.

E.g. it holds in state 2 because: we have to find a least one path P
starting in state 2 (i.e. the first "E" quantifier) such that there is
at least one state s' on P (i.e. the "F" operator) where subformula EG
<x>1 holds in state s'. Let P = 2,0,3,3,3,... and s' = 3. We check if
subformula EG <x>1 holds in s': we have to find at least one path P'
starting in s' (the "E") such that in all states along P' (the "G"
operator) subformula <x>1 holds. Let P' = 3,3,3,... Then <x>1 holds in
every state of P' because <x>1 holds in state 3. Therefore, EF (EG
<x>1) holds in state 2. Checking the other states is similiar: we can
always choose P' = 3,3,3,... for the second "E" in EF (EG <x>1), and
there is a path P to state 3 from every other state for the first "E"
in EF (EG <x>1).