\newcommand{\al}{\square}
\newcommand{\nx}{\bigcirc}
+\everymath{\displaystyle}
+
+\author{Mart Lubbers}
+\date{\today}
+\title{Model Checking Excercises 1}
+
\begin{document}
+\maketitle
\begin{enumerate}
\item
- $\xymatrix{
- \ar[dr]\\
- & *+[o][F-]{s_0}\\
- *+[o][F-]{nc_1} & & *+[o][F-]{nc_1}
- }$
\item
$\al(crit_0\veebar crit_1)$
\item
We define:\\
- $\displaystyle AP=\bigcup_{i\in N}\{lift_n, door_n,call_n\},
+ $ 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)$
+ $\bigwedge_{n\in N}\al(door_m\ra lift_n)$
\item
- $\forall n\in N\al(call_n\ra\ev lift_n)$
+ $\bigwedge_{n\in N}\al(call_n\ra\ev(lift_n\wedge door_n))$
\item
$\al\ev lift_0$
\item
- $\al call_3\rightarrow\bigcirc lift_3$
+ $\al(call_3\rightarrow\bigcirc (lift_3\wedge door_3))$
\end{enumerate}
\item\strut\\
$\begin{array}{ll}