--- /dev/null
+\documentclass{article}
+
+\usepackage{a4wide}
+\usepackage{amssymb}
+\usepackage{amsmath}
+\usepackage{booktabs}
+\usepackage[all]{xypic}
+
+\newcommand{\ra}{\rightarrow}
+\newcommand{\un}{\text{ \textsf{U} }}
+\newcommand{\ev}{\lozenge}
+\newcommand{\al}{\square}
+\newcommand{\nx}{\bigcirc}
+
+\everymath{\displaystyle}
+
+\author{Mart Lubbers}
+\date{\today}
+\title{Model Checking Excercises 2}
+
+\begin{document}
+\maketitle
+\begin{enumerate}
+ \item\strut\\
+ \begin{tabular}{ll}
+ $TS\nvDash\varphi_1$ & $s_1\ra \overline{s_3\ra s_4}$\\
+ $TS\vDash\varphi_2$ & Yes, all loops go via $s_2,s_3$ or $s_5$
+ where $c$ holds.\\
+ $TS\vDash\varphi_3$ & Yes, $\nx\neg c$ is only true when the next
+ state is $s_4$.\\
+ & From $s_4$ you can only go to a state where $c$ holds.\\
+ $TS\nvDash\varphi_4$ & $s_2\ra\ldots$\\
+ $TS\vDash\varphi_5$ & Yes, starting in $s_1$ $b\vee c$ holds after
+ the first transition\\
+ & Starting in $s_2$ $b\vee c$ holds immediatly.\\
+ $TS\vDash\varphi_6$ & $s_1\ra\overline{s_4\ra s_2}$
+ \end{tabular}
+ \item
+ \begin{equation}
+ \xymatrix{
+ \ar[r] &
+ *+[F]{s_0}\ar@/^/[r]^{\neg a}\ar@(d,l)^{a} &
+ *+[F]{s_1}\ar@/^/[l]^{\neg b}\ar[r]^{b} &
+ *+[Fo]{s_2}\ar@(d,r)_{true}
+ }
+ \end{equation}
+
+ \begin{equation}
+ \xymatrix{
+ \ar[r] &
+ *+[Fo]{s_0}\ar@(d,l)^{true}\ar[r]^{a} &
+ *+[F]{s_1}\ar@(d,l)^{true}\\
+ \ar[r] & *+[F]{s_2}\ar@(d,l)^{\emptyset}\ar[r]^{a\vee b} &
+ *+[Fo]{s_3}\ar@(d,l)^{true}
+ }
+ \end{equation}
+
+ \begin{equation}
+ \xymatrix{
+ \ar[r] &
+ *+[Fo]{s_0}\ar[r]^{\neg a}\ar[d]_{a} &
+ *+[F]{s_1}\ar@(d,r)_{true}\\
+ & *+[Fo]{s_2}\ar@(d,l)^{true}
+ }
+ \end{equation}
+ \item
+ $\ev\al(a\wedge\ev b)$
+\end{enumerate}
+\end{document}