From: Mart Lubbers Date: Sun, 21 Feb 2016 15:40:45 +0000 (+0100) Subject: . X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=3d3e5e5928908919179ffa26017ddac147f5ef4e;p=mc1516.git . --- 3d3e5e5928908919179ffa26017ddac147f5ef4e diff --cc Makefile index 1c8e48e,3fbb9ab..b834717 --- a/Makefile +++ b/Makefile @@@ -1,6 -1,6 +1,6 @@@ LATEX:=latex DOT:=dot - DOCUMENTS:=e1.pdf -DOCUMENTS:=e1.pdf e2.pdf ++DOCUMENTS:=e1.pdf e2.pdf e3.pdf .PHONY: all clean clobber graphs diff --cc e3.tex index 0000000,0000000..33bcca5 new file mode 100644 --- /dev/null +++ b/e3.tex @@@ -1,0 -1,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}