product automaton

diff --git a/e3.tex b/e3.tex
index 33bcca5..4bce446 100644 (file)
--- a/e3.tex
+++ b/e3.tex
@@ -21,13 +21,23 @@
 \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\}\text{ thus }\Phi_1\text{ is satisfied}$
+               \{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))\\
@@ -37,6 +47,7 @@
                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)))$$
@@ -45,13 +56,29 @@
                        \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 & 
+                       & :=\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}