e3.tex

   1 \documentclass{article}
   2
   3 \usepackage{a4wide}
   4 \usepackage{amssymb}
   5 \usepackage{amsmath}
   6 \usepackage[all]{xypic}
   7
   8 \newcommand{\ra}{\rightarrow}
   9 \newcommand{\un}{\text{ \textsf{U} }}
  10 \newcommand{\ev}{\lozenge}
  11 \newcommand{\al}{\square}
  12 \newcommand{\nx}{\bigcirc}
  13
  14 \everymath{\displaystyle}
  15
  16 \author{Mart Lubbers}
  17 \date{\today}
  18 \title{Model Checking Excercises 3}
  19
  20 \begin{document}
  21 \maketitle
  22 \begin{enumerate}
  23         \item
  24         \item
  25                 $\text{TS}\vDash\Phi_1\Leftrightarrow \{s_0\}\subseteq Sat(
  26                         \exists\ev\forall\al c)\\
  27                 Sat(c)= \{s_3, s_4\}\\
  28                 Sat(\forall\al (s_3\vee s_4))= \{s_4\}\\
  29                 Sat(\exists\ev(s_4)= \{s_0,s_1\}\\
  30                 \{s_0\}\subseteq \{s_0,s_1\}\text{ thus }\Phi_1\text{ is satisfied}$
  31                 \\\strut\\
  32                 $\text{TS}\vDash\Phi_2\Leftrightarrow \{s_0\}\subseteq Sat(
  33                         \forall(a\un \forall\ev c))\\
  34                 Sat(c)= \{s_3, s_4\}\\
  35                 Sat(\forall\ev(s_3\vee s_4))=\{s_0,s_1,s_4\}\\
  36                 Sat(a)= \{s_0, s_1\}\\
  37                 Sat(\forall(a\un \forall\ev c))=\{s_0,s_1,s_4\}\\
  38                 \{s_0\}\subseteq \{s_0,s_1,s_4\}\text{ thus }\Phi_2\text{ is satisfied} $
  39         \item
  40
  41         \item
  42                 For formula:
  43                 $$\varphi:=\al(a\ra(\neg b\un(a\wedge b)))$$
  44                 We create an automaton $\neg\varphi$ where
  45                 $$\begin{array}{rlr}
  46                         \neg\varphi
  47                         & :=\ev\neg(a\ra(\neg b\un(a\wedge b)))\\
  48                         & :=\ev(a\wedge\neg(\neg b\un(a\wedge b)))\\
  49                         & :=\ev(a\wedge(\al\neg b\vee(\neg b\un(a\wedge b))))\\
  50                         & :=\ev(a\wedge\al\neg b)\vee\ev(a\wedge(\neg b\un(a\wedge b)))\\
  51                         & :=\ev(a\wedge\neg\ev b) & \ev(a\wedge(\neg b\un(a\wedge b)))\\
  52                 \end{array}$$
  53                 Elementary sets for $\varphi=\ev(a\wedge\neg\ev b)$ where
  54                 $\psi=a\wedge\neg\ev b$:
  55                 $$\begin{array}{llll}
  56                         a & b & \varphi & \ev\psi\\
  57                         a & b & \varphi & \ev\psi\\
  58                 \end{array}$$
  59 \end{enumerate}
  60 \end{document}