a2/3.tex

   1 \section{Problem 3}
   2 \emph{The goal of this problem is to exploit the power of the recom mended
   3 tools rather than elaborating the questions by hand.}
   4 \begin{enumerate}[a.]
   5         \item\emph{In mathematics, a \emph{group} is defined to be a set $G$
   6                 with an element $I\in G$, a binary operator $∗$ and a unary
   7                 operator inv satisfying.
   8                 $$x*(y*z)=(x*y)*z, x*I=x\text{ and }x*inv(x)=I,$$
   9                 for all $x,y,z\in G$. Determine whether in every group each of
  10                 the four properties
  11                 $$I*x=x, inv(inv(x))=x, inv(x)*x=I\text{ and } x*y=y*x$$
  12                 holds for all $x,y\in G$. If a property does not hold,
  13                 determine the size of the smallest finite group for which it
  14                 does not hold.}
  15         \item\emph{A term rewrite sysetm consists of the single rule
  16                 $$a(x,a(y,a(z,u)))\rightarrow a(y,a(z,a(x,u))),$$
  17                 in which $a$ is a binary symbol and $x,y,z,u$ are variables.
  18                 Moreover, there are constants $b,c,d,e,f,g$. Determine whether
  19                 $c$ and $d$ may swapped in $a(b,a(c,a(d,a(e,a(f,a(b,g))))))$ by
  20                 rewriting, that is, $a(b,a(c,a(d,a(e,a(f,a(b,g))))))$ rewrites
  21                 in a finite number of steps to
  22                 $a(b,a(d,a(c,a(e,a(f,a(b,g))))))$.}\\
  23
  24                 When inspecting the rewrite rule more closely we see that the
  25                 entire structure of the formula stays the same and that only
  26                 the variables $x,y,z$ are changed in order. Because of this we
  27                 can simplify the rule to
  28                 $$x,y,z\rightarrow y,z,x$$
  29                 and we can simplify the question to asking whether
  30                 $b,c,d,e,f,b$ rewrites to $b,d,c,e,f,b$.\\
  31
  32                 Because of this the nature of the rewritten problem becomes
  33                 solvable by a symbolic model checker. We define for every
  34                 position $i\in\{0\ldots5\}$ a variable $p_i$ of the enumeration
  35                 type $\{b,c,d,e,f\}$. To keep track of the moves we define a
  36                 move $m\in\{0\ldots4\}$ variable that indicates the location of
  37                 the first variable or $0$ for the initial value.  The initial
  38                 values of the position variables is
  39                 $$p_0=b,p_1=c,p_2=d,p_3=e,p_4=f,p_5=b$$
  40                 There are four possible transitions and they are put in a
  41                 disjuction and shown below:
  42                 $$\begin{array}{rl}
  43                         next(m)=1 \wedge & next(p_0)=p_1 \wedge next(p_1)=p_2
  44                                 \wedge next(p_2)=p_0 \wedge\\
  45                         & next(p_3)=p_3 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5\\
  46
  47                         next(m)=2 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_2
  48                                 \wedge next(p_2)=p_3 \wedge\\
  49                         & next(p_3)=p_1 \wedge next(p_4)=p_4 \wedge next(p_5)=p_5\\
  50
  51                         next(m)=3 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_1
  52                                 \wedge next(p_2)=p_3 \wedge\\
  53                         & next(p_3)=p_4 \wedge next(p_4)=p_2 \wedge next(p_5)=p_5\\
  54                         next(m)=4 \wedge & next(p_0)=p_0 \wedge next(p_1)=p_1
  55                                 \wedge next(p_2)=p_2 \wedge\\
  56                         & next(p_3)=p_4 \wedge next(p_4)=p_5 \wedge next(p_5)=p_3
  57                 \end{array}$$
  58
  59                 The LTL logic goal state would then be
  60                 $$\mathcal{G} \neg(p_0=b\wedge p_1=d\wedge p_2=c\wedge
  61                 p_3=e\wedge p_4=f\wedge p_5=b)$$
  62
  63                 The solution described below is found by
  64                 \textsc{NuSMV} within $0.01$ seconds. Overline triples are the
  65                 ones changed in the next.
  66                 $$\begin{array}{rl}
  67                         \overline{b,c,d},e,f,b
  68                                 & \rightarrow c,d,\overline{b,e,f},b\\
  69                                 & \rightarrow c,d,e,\overline{f,b,b}\\
  70                                 & \rightarrow c,d,e,\overline{b,b,f}\\
  71                                 & \rightarrow c,\overline{d,e,b},f,b\\
  72                                 & \rightarrow c,\overline{e,b,d},f,b\\
  73                                 & \rightarrow \overline{c,b,d},e,f,b\\
  74                                 & \rightarrow b,\overline{d,c,e},f,b\\
  75                                 & \rightarrow b,c,e,d,f,b\\
  76                 \end{array}$$
  77
  78
  79
  80 \end{enumerate}