.

diff --git a/Makefile b/Makefile
index 3fbb9ab..b834717 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,6 @@
 LATEX:=latex
 DOT:=dot
-DOCUMENTS:=e1.pdf e2.pdf
+DOCUMENTS:=e1.pdf e2.pdf e3.pdf
 
 .PHONY: all clean clobber graphs
 

diff --git a/e3.tex b/e3.tex
new file mode 100644 (file)
index 0000000..33bcca5
--- /dev/null
+++ b/e3.tex
@@ -0,0 +1,57 @@
+\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
+       \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\}\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(\al\neg b\vee
+                               
+                               
+               \end{array}$$
+               Elementary sets:
+               $$\begin{array}{lll}
+                       a & b & 
+               \end{array}$$
+\end{enumerate}
+\end{document}