mbt_exercises/mbt.tex

   1 %&mbt
   2 \begin{document}
   3
   4 \section{Theory of Labelled Transition Systems}
   5 \subsection{Testing equivalences}
   6 \begin{enumerate}[a)]
   7         \item $\bordermatrix{
   8                         ~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5\cr
   9                         Q_1 & 1\cr
  10                         Q_2 & 0 & 1\cr
  11                         Q_3 & 0 & 0 & 1\cr
  12                         Q_4 & 0 & 0 & 0 & 1\cr
  13                         Q_5 & 0 & 0 & 0 & 0 & 1\cr
  14                 }$
  15         \item $\bordermatrix{
  16                         ~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5\cr
  17                         Q_1 & 1\cr
  18                         Q_2 & 0 & 1\cr
  19                         Q_3 & 0 & 1 & 1\cr
  20                         Q_4 & 0 & 1 & 1 & 1\cr
  21                         Q_5 & 0 & 1 & 1 & 1 & 1\cr
  22                 }$
  23         \item $\bordermatrix{
  24                         ~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5\cr
  25                         Q_1 & 1\cr
  26                         Q_2 & 0 & 1\cr
  27                         Q_3 & 0 & 1 & 1\cr
  28                         Q_4 & 0 & 1 & 1 & 1\cr
  29                         Q_5 & 0 & 1 & 1 & 1 & 1\cr
  30                 }$
  31         \item You can discriminate $Q_1$ from all the others by running the
  32                 trace $a\rightarrow c$. $Q_2$ can be discriminated from the
  33                 rest by running $a\rightarrow b\rightarrow c$ because
  34                 $Q_3,Q_4$ and $Q_5$ may refuse the last $c$. To
  35                 discriminate $Q_3$ you can run $a\rightarrow c$ since
  36                 $Q_4$ and $Q_5$ may refuse $c$. To discriminate $Q_4$ you need
  37                 to be able to go back. You can then discriminate by running
  38                 $a\rightarrow c$ and then go back and run $b\rightarrow c$.
  39                 This trace can only be accepted by $Q_4$.
  40         \item $\bordermatrix{
  41                         ~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5\cr
  42                         Q_1 & 1\cr
  43                         Q_2 & 0 & 1\cr
  44                         Q_3 & 0 & 0 & 1\cr
  45                         Q_4 & 0 & 1 & 1 & 1\cr
  46                         Q_5 & 0 & 1 & 1 & 1 & 1\cr
  47                 }$
  48         \item See $d)$.
  49         \item $\bordermatrix{
  50                         ~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5\cr
  51                         Q_1 & 1\cr
  52                         Q_2 & 0 & 1\cr
  53                         Q_3 & 0 & 0 & 1\cr
  54                         Q_4 & 0 & 0 & 0 & 1\cr
  55                         Q_5 & 0 & 0 & 0 & 1 & 1\cr
  56                 }$
  57         \item All processes as explained in $d)$.
  58         \item $\bordermatrix{
  59                         i\setminus s & Q_1 & Q_2 & Q_3 & Q_4 & Q_5\cr
  60                         Q_1 & 1 & 0 & 0 & 0 & 0\cr
  61                         Q_2 & 1 & 1 & 1 & 1 & 1\cr
  62                         Q_3 & 1 & 1 & 1 & 1 & 1\cr
  63                         Q_4 & 1 & 1 & 1 & 1 & 1\cr
  64                         Q_5 & 1 & 1 & 1 & 1 & 1\cr
  65                 }$
  66 \end{enumerate}
  67
  68 \subsection{Testing equivalences}
  69 \begin{enumerate}[a)]
  70         \item $\bordermatrix{
  71                         ~ & P_1 & P_2 & P_3 & P_4\cr
  72                         P_1 & 1\cr
  73                         P_2 & 0 & 1\cr
  74                         P_3 & 0 & 0 & 1\cr
  75                         P_4 & 0 & 0 & 0 & 1\cr
  76                 }$
  77         \item $\bordermatrix{
  78                         ~ & P_1 & P_2 & P_3 & P_4\cr
  79                         P_1 & 1\cr
  80                         P_2 & 0 & 1\cr
  81                         P_3 & 0 & 1 & 1\cr
  82                         P_4 & 0 & 1 & 1 & 1\cr
  83                 }$
  84         \item Trace $a\rightarrow b\rightarrow c$ may refuse in $P_3$ and $P_4$
  85                 but not in $P_2$. $P_3$ and $P_4$ can only be distinguished if
  86                 you are allowed to go back. If the trace $a\rightarrow
  87                 b\rightarrow c$ accepts you can go back to the state after $a$
  88                 and try $b\rightarrow d$. This might only accept in $P_3$.
  89         \item $\bordermatrix{
  90                         ~ & P_1 & P_2 & P_3 & P_4\cr
  91                         P_1 & 1\cr
  92                         P_2 & 0 & 1\cr
  93                         P_3 & 0 & 0 & 1\cr
  94                         P_4 & 0 & 0 & 1 & 1\cr
  95                 }$
  96         \item All processes.
  97         \item $\bordermatrix{
  98                         i\setminus s& P_1 & P_2 & P_3 & P_4\cr
  99                         P_1 & 1 & 0 & 0 & 0\cr
 100                         P_2 & 0 & 1 & \cr
 101                         P_3 & 0 & 0 & 1\cr
 102                         P_4 & 0 & 0 & 1 & 1\cr
 103                 }$
 104         \item
 105                 $P_1=\xymatrix{
 106                         \ar[dr]&\\
 107                                & s_0\ar[d]^a\\
 108                                & s_1\ar[d]^b\\
 109                                & s_2\ar[d]^c\\
 110                                & s_3\\
 111                 }$
 112                 $P_2=\xymatrix{
 113                         \ar[dr]&\\
 114                                & s_0\ar[d]^a\\
 115                                & s_1\ar[d]^b\\
 116                                & s_2\ar[dl]^c\ar[dr]^d\\
 117                         s_3    & & s_4\\
 118                 }$
 119                 $P_3=\xymatrix{
 120                         \ar[dr]     &\\
 121                                     & s_0\ar[d]^a\\
 122                                     & s_1\ar[dl]^b\ar[dr]^b\\
 123                         s_2\ar[d]^c & & s_3\ar[d]^d\\
 124                         s_4         & & s_5\\
 125                 }$
 126                 $P_4=\xymatrix{
 127                         \ar[dr]     &\\
 128                                     & s_0\ar[dl]^a\ar[dr]^a\\
 129                         s_2\ar[d]^b & & s_3\ar[d]^b\\
 130                         s_4\ar[d]^c & & s_5\ar[d]^d\\
 131                         s_6         & & s_7
 132                 }$
 133 \end{enumerate}
 134
 135 \subsection{Testing equivalences}
 136 \subsection{Testing equivalences}
 137 \subsection{Testing equivalences}
 138
 139 \end{document}