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}
20 *+
[o
][F-
]{nc_1
} & & *+
[o
][F-
]{nc_1
}
23 $
\al(crit_0
\veebar crit_1)$
26 $
\displaystyle AP=
\bigcup_{i
\in N
}\
{lift_n, door_n,call_n\
},
30 $
\forall n
\in N
\al(door_m
\ra lift_n)$
32 $
\forall n
\in N
\al(call_n
\ra\ev lift_n)$
36 $
\al call_3
\rightarrow\bigcirc lift_3$
41 s_2
\ra s_4
\overline{\ra s_5
}\\
43 s_2
\ra s_4
\overline{\ra s_5
}\\
44 \varphi_3=
\nx\neg c
\rightarrow\nx\nx c &
45 s_2
\ra s_4
\overline{\ra s_5
}\\
47 \text{Impossible. $a$ only holds in $s_1$ and in $s_5$.
}\\
48 &
\text{$s_1$ we can only leave through a state where $
\neg a$
}\\
49 &
\text{$s_5$ we can not reach through $s_1$ without passing
50 through a $
\neg a$ state
}\\
51 \varphi_5=a
\un\al(b
\vee c) &
52 s_1
\ra s_4
\overline{\ra s_5
}\\
53 \varphi_6=(
\nx\nx b)
\un(b
\vee c) &
54 s_2
\ra s_4
\overline{\ra s_5
}