\documentclass{article}

\usepackage{a4wide}
\usepackage{amssymb}
\usepackage{amsmath}
\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 3}

\begin{document}
\maketitle
\begin{enumerate}
	\item
		$\begin{array}{rl}
			\Psi_1 
			& =\exists\ev\forall\al c\\
			& =\exists(true\un\forall\al c)\\
			& =\exists(true\un\neg\exists\ev\neg c)\\
			& =\exists(true\un\neg\exists(true\un \neg c))\\
			\Psi_2
			& =\forall(a\un\forall\ev c)\\
			\ldots
		\end{array}$
	\item 
		$\text{TS}\vDash\Phi_1\Leftrightarrow \{s_0\}\subseteq Sat(
			\exists\ev\forall\al c)\\
		Sat(c)= \{s_3, s_4\}\\
		Sat(\forall\al (s_3\vee s_4))= \{s_4\}\\
		Sat(\exists\ev(s_4)= \{s_0,s_1\}\\
		\{s_0\}\subseteq \{s_0,s_1,s_4\}\text{ thus }\Phi_1\text{ is satisfied}$
		\\\strut\\
		$\text{TS}\vDash\Phi_2\Leftrightarrow \{s_0\}\subseteq Sat(
			\forall(a\un \forall\ev c))\\
		Sat(c)= \{s_3, s_4\}\\
		Sat(\forall\ev(s_3\vee s_4))=\{s_0,s_1,s_4\}\\
		Sat(a)= \{s_0, s_1\}\\
		Sat(\forall(a\un \forall\ev c))=\{s_0,s_1,s_4\}\\
		\{s_0\}\subseteq \{s_0,s_1,s_4\}\text{ thus }\Phi_2\text{ is satisfied} $
	\item 

	\item
		For formula:
		$$\varphi:=\al(a\ra(\neg b\un(a\wedge b)))$$
		We create an automaton $\neg\varphi$ where
		$$\begin{array}{rl}
			\neg\varphi 
			& :=\ev\neg(a\ra(\neg b\un(a\wedge b)))\\
			& :=\ev(a\wedge\neg(\neg b\un(a\wedge b)))\\
			& :=\ev(a\wedge\neg\ev b\vee(\neg b\un(b\wedge \neg a)))
		\end{array}$$
		$$\xymatrix{
			\ar[r] & 
				*+[Fo]{q_0}
					\ar[r]^{a\wedge\neg b}
					\ar@(ul,ur)^{\neg a}
					\ar[d]^{a\wedge b} &
				*+[F]{q_2}
					\ar@(ul,ur)^{\neg b}
					\ar[d]^{b\vee\neg a}\\
			  	& *+[Fo]{q_1} \ar@(dl,ul)^{true}
			  	& *+[F]{q_3} \ar@(dr,ur)_{true}
		}$$
		Which leads to the following product TS:
		$$\xymatrix{
			\ar[dr] & s_0 & s_1 & s_2 & s_3\\
			q_0 & *+[Fo]{}\ar[r]\ar[ddrrr]   & *+[Fo]{}\ar[dr]\\
			q_1 & *+[Fo]{}\ar[r]\ar@/_/[rrr] & *+[Fo]{}\ar[r] & *+[Fo]{}\ar@(u,r)\ar[r] & *+[Fo]{}\ar@/^/[lll]\\
			q_2 & *+[F]{}\ar@/_/[rrr]\ar[dr] &                &                         & *+[F]{}\ar@/^/[lll]\\
			q_3 & *+[F]{}\ar@/_/[rrr]\ar[r]  & *+[F]{}\ar[r]  & *+[F]{}\ar@(u,r)\ar[r]  & *+[F]{}\ar@/^/[lll]
		}$$
		Thus forexample the path: $(s_0s_3)^{\omega}$ is a counterexample.

\end{enumerate}
\end{document}
