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                 $\begin{array}{rl}
  25                         \Psi_1
  26                         & =\exists\ev\forall\al c\\
  27                         & =\exists(true\un\forall\al c)\\
  28                         & =\exists(true\un\neg\exists\ev\neg c)\\
  29                         & =\exists(true\un\neg\exists(true\un \neg c))\\
  30                         \Psi_2
  31                         & =\forall(a\un\forall\ev c)\\
  32                         \ldots
  33                 \end{array}$
  34         \item
  35                 $\text{TS}\vDash\Phi_1\Leftrightarrow \{s_0\}\subseteq Sat(
  36                         \exists\ev\forall\al c)\\
  37                 Sat(c)= \{s_3, s_4\}\\
  38                 Sat(\forall\al (s_3\vee s_4))= \{s_4\}\\
  39                 Sat(\exists\ev(s_4)= \{s_0,s_1\}\\
  40                 \{s_0\}\subseteq \{s_0,s_1,s_4\}\text{ thus }\Phi_1\text{ is satisfied}$
  41                 \\\strut\\
  42                 $\text{TS}\vDash\Phi_2\Leftrightarrow \{s_0\}\subseteq Sat(
  43                         \forall(a\un \forall\ev c))\\
  44                 Sat(c)= \{s_3, s_4\}\\
  45                 Sat(\forall\ev(s_3\vee s_4))=\{s_0,s_1,s_4\}\\
  46                 Sat(a)= \{s_0, s_1\}\\
  47                 Sat(\forall(a\un \forall\ev c))=\{s_0,s_1,s_4\}\\
  48                 \{s_0\}\subseteq \{s_0,s_1,s_4\}\text{ thus }\Phi_2\text{ is satisfied} $
  49         \item
  50
  51         \item
  52                 For formula:
  53                 $$\varphi:=\al(a\ra(\neg b\un(a\wedge b)))$$
  54                 We create an automaton $\neg\varphi$ where
  55                 $$\begin{array}{rl}
  56                         \neg\varphi
  57                         & :=\ev\neg(a\ra(\neg b\un(a\wedge b)))\\
  58                         & :=\ev(a\wedge\neg(\neg b\un(a\wedge b)))\\
  59                         & :=\ev(a\wedge\neg\ev b\vee(\neg b\un(b\wedge \neg a)))
  60                 \end{array}$$
  61                 $$\xymatrix{
  62                         \ar[r] &
  63                                 *+[Fo]{q_0}
  64                                         \ar[r]^{a\wedge\neg b}
  65                                         \ar@(ul,ur)^{\neg a}
  66                                         \ar[d]^{a\wedge b} &
  67                                 *+[F]{q_2}
  68                                         \ar@(ul,ur)^{\neg b}
  69                                         \ar[d]^{b\vee\neg a}\\
  70                                 & *+[Fo]{q_1} \ar@(dl,ul)^{true}
  71                                 & *+[F]{q_3} \ar@(dr,ur)_{true}
  72                 }$$
  73                 Which leads to the following product TS:
  74                 $$\xymatrix{
  75                         \ar[dr] & s_0 & s_1 & s_2 & s_3\\
  76                         q_0 & *+[Fo]{}\ar[r]\ar[ddrrr]   & *+[Fo]{}\ar[dr]\\
  77                         q_1 & *+[Fo]{}\ar[r]\ar@/_/[rrr] & *+[Fo]{}\ar[r] & *+[Fo]{}\ar@(u,r)\ar[r] & *+[Fo]{}\ar@/^/[lll]\\
  78                         q_2 & *+[F]{}\ar@/_/[rrr]\ar[dr] &                &                         & *+[F]{}\ar@/^/[lll]\\
  79                         q_3 & *+[F]{}\ar@/_/[rrr]\ar[r]  & *+[F]{}\ar[r]  & *+[F]{}\ar@(u,r)\ar[r]  & *+[F]{}\ar@/^/[lll]
  80                 }$$
  81                 Thus forexample the path: $(s_0s_3)^{\omega}$ is a counterexample.
  82
  83 \end{enumerate}
  84 \end{document}