1 \documentclass{article
}
6 \usepackage[all
]{xypic
}
8 \newcommand{\ra}{\rightarrow}
9 \newcommand{\un}{\text{ \textsf{U
} }}
10 \newcommand{\ev}{\lozenge}
11 \newcommand{\al}{\square}
12 \newcommand{\nx}{\bigcirc}
14 \everymath{\displaystyle}
18 \title{Model Checking Excercises
1}
25 $
\al(crit_0
\veebar crit_1)$
28 $ AP=
\bigcup_{i
\in N
}\
{lift_n, door_n,call_n\
},
32 $
\bigwedge_{n
\in N
}\al(door_m
\ra lift_n)$
34 $
\bigwedge_{n
\in N
}\al(call_n
\ra\ev(lift_n
\wedge door_n))$
38 $
\al(call_3
\rightarrow\bigcirc (lift_3
\wedge door_3))$
43 s_2
\ra s_4
\overline{\ra s_5
}\\
45 s_2
\ra s_4
\overline{\ra s_5
}\\
46 \varphi_3=
\nx\neg c
\rightarrow\nx\nx c &
47 s_2
\ra s_4
\overline{\ra s_5
}\\
49 \text{Impossible. $a$ only holds in $s_1$ and in $s_5$.
}\\
50 &
\text{$s_1$ we can only leave through a state where $
\neg a$
}\\
51 &
\text{$s_5$ we can not reach through $s_1$ without passing
52 through a $
\neg a$ state
}\\
53 \varphi_5=a
\un\al(b
\vee c) &
54 s_1
\ra s_4
\overline{\ra s_5
}\\
55 \varphi_6=(
\nx\nx b)
\un(b
\vee c) &
56 s_2
\ra s_4
\overline{\ra s_5
}