\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}
