\usepackage{a4wide}
\usepackage{amssymb}
\usepackage{amsmath}
+\usepackage[all]{xypic}
\newcommand{\ra}{\rightarrow}
\newcommand{\un}{\text{ \textsf{U} }}
\begin{document}
\begin{enumerate}
\item
+ $\xymatrix{
+ \ar[dr]\\
+ & *+[o][F-]{s_0}\\
+ *+[o][F-]{nc_1} & & *+[o][F-]{nc_1}
+ }$
\item
- \item
+ $\al(crit_0\veebar crit_1)$
+ \item
+ We define:\\
+ $\displaystyle AP=\bigcup_{i\in N}\{lift_n, door_n,call_n\},
+ N=\{0, 1, 2, 3\}$
+ \begin{enumerate}
+ \item
+ $\forall n\in N\al(door_m\ra lift_n)$
+ \item
+ $\forall n\in N\al(call_n\ra\ev lift_n)$
+ \item
+ $\al\ev lift_0$
+ \item
+ $\al call_3\rightarrow\bigcirc lift_3$
+ \end{enumerate}
\item\strut\\
$\begin{array}{ll}
- \phi_1=\ev\al c &
+ \varphi_1=\ev\al c &
s_2\ra s_4\overline{\ra s_5}\\
- \phi_2=\al\ev c &
+ \varphi_2=\al\ev c &
s_2\ra s_4\overline{\ra s_5}\\
- \phi_3=\nx\neg c\rightarrow\nx\nx c &
+ \varphi_3=\nx\neg c\rightarrow\nx\nx c &
s_2\ra s_4\overline{\ra s_5}\\
- \phi_4=\al a &
+ \varphi_4=\al a &
\text{Impossible. $a$ only holds in $s_1$ and in $s_5$.}\\
& \text{$s_1$ we can only leave through a state where $\neg a$}\\
& \text{$s_5$ we can not reach through $s_1$ without passing
through a $\neg a$ state}\\
- \phi_5=a\un\al(b\vee c) &
+ \varphi_5=a\un\al(b\vee c) &
s_1\ra s_4\overline{\ra s_5}\\
- \phi_6=(\nx\nx b)\un(b\vee c) &
+ \varphi_6=(\nx\nx b)\un(b\vee c) &
s_2\ra s_4\overline{\ra s_5}
\end{array}$
\end{enumerate}