mbt_exercises/mbt.tex

   1 %&mbt
   2 \begin{document}
   3
   4 % 1
   5 \section{Theory of Labelled Transition Systems}
   6
   7 % 1.1
   8 \subsection{Testing equivalences}
   9 \begin{enumerate}[a)]
  10         \item $\bordermatrix{
  11                         ~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5\cr
  12                         Q_1 & 1\cr
  13                         Q_2 & 0 & 1\cr
  14                         Q_3 & 0 & 0 & 1\cr
  15                         Q_4 & 0 & 0 & 0 & 1\cr
  16                         Q_5 & 0 & 0 & 0 & 0 & 1\cr
  17                 }$
  18         \item $\bordermatrix{
  19                         ~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5\cr
  20                         Q_1 & 1\cr
  21                         Q_2 & 0 & 1\cr
  22                         Q_3 & 0 & 1 & 1\cr
  23                         Q_4 & 0 & 1 & 1 & 1\cr
  24                         Q_5 & 0 & 1 & 1 & 1 & 1\cr
  25                 }$
  26         \item $\bordermatrix{
  27                         ~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5\cr
  28                         Q_1 & 1\cr
  29                         Q_2 & 0 & 1\cr
  30                         Q_3 & 0 & 1 & 1\cr
  31                         Q_4 & 0 & 1 & 1 & 1\cr
  32                         Q_5 & 0 & 1 & 1 & 1 & 1\cr
  33                 }$
  34         \item You can discriminate $Q_1$ from all the others by running the
  35                 trace $a\rightarrow c$. $Q_2$ can be discriminated from the
  36                 rest by running $a\rightarrow b\rightarrow c$ because
  37                 $Q_3,Q_4$ and $Q_5$ may refuse the last $c$. To
  38                 discriminate $Q_3$ you can run $a\rightarrow c$ since
  39                 $Q_4$ and $Q_5$ may refuse $c$. To discriminate $Q_4$ you need
  40                 to be able to go back. You can then discriminate by running
  41                 $a\rightarrow c$ and then go back and run $b\rightarrow c$.
  42                 This trace can only be accepted by $Q_4$.
  43         \item $\bordermatrix{
  44                         ~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5\cr
  45                         Q_1 & 1\cr
  46                         Q_2 & 0 & 1\cr
  47                         Q_3 & 0 & 0 & 1\cr
  48                         Q_4 & 0 & 1 & 1 & 1\cr
  49                         Q_5 & 0 & 1 & 1 & 1 & 1\cr
  50                 }$
  51         \item See $d)$.
  52         \item $\bordermatrix{
  53                         ~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5\cr
  54                         Q_1 & 1\cr
  55                         Q_2 & 0 & 1\cr
  56                         Q_3 & 0 & 0 & 1\cr
  57                         Q_4 & 0 & 0 & 0 & 1\cr
  58                         Q_5 & 0 & 0 & 0 & 1 & 1\cr
  59                 }$
  60         \item All processes as explained in $d)$.
  61         \item $\bordermatrix{
  62                         i\setminus s & Q_1 & Q_2 & Q_3 & Q_4 & Q_5\cr
  63                         Q_1 & 1 & 0 & 0 & 0 & 0\cr
  64                         Q_2 & 1 & 1 & 1 & 1 & 1\cr
  65                         Q_3 & 1 & 1 & 1 & 1 & 1\cr
  66                         Q_4 & 1 & 1 & 1 & 1 & 1\cr
  67                         Q_5 & 1 & 1 & 1 & 1 & 1\cr
  68                 }$
  69 \end{enumerate}
  70
  71 % 1.2
  72 \subsection{Testing equivalences}
  73 \begin{enumerate}[a)]
  74         \item $\bordermatrix{
  75                         ~ & P_1 & P_2 & P_3 & P_4\cr
  76                         P_1 & 1\cr
  77                         P_2 & 0 & 1\cr
  78                         P_3 & 0 & 0 & 1\cr
  79                         P_4 & 0 & 0 & 0 & 1\cr
  80                 }$
  81         \item $\bordermatrix{
  82                         ~ & P_1 & P_2 & P_3 & P_4\cr
  83                         P_1 & 1\cr
  84                         P_2 & 0 & 1\cr
  85                         P_3 & 0 & 1 & 1\cr
  86                         P_4 & 0 & 1 & 1 & 1\cr
  87                 }$
  88         \item Trace $a\rightarrow b\rightarrow c$ may refuse in $P_3$ and $P_4$
  89                 but not in $P_2$. $P_3$ and $P_4$ can only be distinguished if
  90                 you are allowed to go back. If the trace $a\rightarrow
  91                 b\rightarrow c$ accepts you can go back to the state after $a$
  92                 and try $b\rightarrow d$. This might only accept in $P_3$.
  93         \item $\bordermatrix{
  94                         ~ & P_1 & P_2 & P_3 & P_4\cr
  95                         P_1 & 1\cr
  96                         P_2 & 0 & 1\cr
  97                         P_3 & 0 & 0 & 1\cr
  98                         P_4 & 0 & 0 & 1 & 1\cr
  99                 }$
 100         \item All processes.
 101         \item $\bordermatrix{
 102                         i\setminus s& P_1 & P_2 & P_3 & P_4\cr
 103                         P_1 & 1 & 0 & 0 & 0\cr
 104                         P_2 & 0 & 1 & 0 & 0\cr
 105                         P_3 & 0 & 0 & 1 & 0\cr
 106                         P_4 & 0 & 0 & 1 & 1\cr
 107                 }$
 108         \item
 109                 $P_1=\xymatrix@C=1pc@R=1pc{
 110                         \ar[dr]&\\
 111                                 & *+[o][F-]{s_0}\ar[d]^a\\
 112                                 & *+[o][F-]{s_1}\ar[d]^b\\
 113                                 & *+[o][F-]{s_2}\ar[d]^c\\
 114                                 & *+[o][F-]{s_3}\\
 115                 }$
 116                 $P_2=\xymatrix@C=1pc@R=1pc{
 117                         \ar[dr]&\\
 118                                 & *+[o][F-]{s_0}\ar[d]^a\\
 119                                 & *+[o][F-]{s_1}\ar[d]^b\\
 120                                 & *+[o][F-]{s_2}\ar[dl]_c\ar[dr]^d\\
 121                         *+[o][F-]{s_3} & & *+[o][F-]{s_4}\\
 122                 }$
 123                 $P_3=\xymatrix@C=1pc@R=1pc{
 124                         \ar[dr] &\\
 125                                 & *+[o][F-]{s_0}\ar[d]^a\\
 126                                 & *+[o][F-]{s_1}\ar[dl]_b\ar[dr]^b\\
 127                         *+[o][F-]{s_2}\ar[d]^c & & *+[o][F-]{s_3}\ar[d]^d\\
 128                         *+[o][F-]{s_4} & & *+[o][F-]{s_5}\\
 129                 }$
 130                 $P_4=\xymatrix@C=1pc@R=1pc{
 131                         \ar[dr] &\\
 132                                 & *+[o][F-]{s_0}\ar[dl]_a\ar[dr]^a\\
 133                         *+[o][F-]{s_2}\ar[d]^b & & *+[o][F-]{s_3}\ar[d]^b\\
 134                         *+[o][F-]{s_4}\ar[d]^c & & *+[o][F-]{s_5}\ar[d]^d\\
 135                         *+[o][F-]{s_6} & & *+[o][F-]{s_7}
 136                 }$
 137 \end{enumerate}
 138
 139 % 1.3
 140 \subsection{Testing equivalences}
 141 \begin{enumerate}[a)]
 142         \item
 143                 \begin{align*}
 144                         \sigma\in traces(p)\leftrightarrow
 145                                 p\text{ \bf after }\sigma\text{ \bf refuses }\emptyset\\
 146                         \sigma\in traces(p)\leftrightarrow
 147                                 \exists p':p\overset{\sigma}{\Rightarrow}p'\text{ and }\forall a\in
 148                                 \emptyset:p'\cancel{\overset{a}{\rightarrow}} & & 2.\\
 149                         \sigma\in traces(p)\leftrightarrow
 150                                 \exists p':p\overset{\sigma}{\Rightarrow}p'\\
 151                         \sigma\in \{\sigma\in L^*|p\overset{\sigma}{\Rightarrow}\}\leftrightarrow
 152                                 \exists p':p\overset{\sigma}{\Rightarrow}p'& & \square\\
 153                 \end{align*}
 154         \item
 155                 \begin{align*}
 156                         p\text{ \bf after }\sigma\text{ \bf refuses } A\leftrightarrow
 157                                 \sigma\cdot A\in Ftraces(p)\\
 158                         \exists p':p\overset{\sigma}{\Rightarrow}p'\text{ and }\forall a\in
 159                                 A:p'\cancel{\overset{a}{\rightarrow}} \leftrightarrow
 160                                 \sigma\cdot A\in Ftraces(p) & & 2.\\
 161                         \exists p':p\overset{\sigma}{\Rightarrow}p'\text{ and }\forall a\in
 162                                 A:p'\cancel{\overset{a}{\rightarrow}} \leftrightarrow
 163                                 \sigma\cdot A\in \{\psi\in(L\cup
 164                                 \mathcal{P}(L))^*|p\overset{\sigma}{\Rightarrow}\} & & 4.\\
 165                 \end{align*}
 166         \item
 167                 \begin{align*}
 168                 \end{align*}
 169         \item
 170                 \begin{align*}
 171                 \end{align*}
 172 \end{enumerate}
 173
 174 % 1.4
 175 \subsection{Testing equivalences}
 176 \begin{enumerate}[a)]
 177         \item $Q:=\xymatrix@C=1pc@R=1pc{
 178                         \ar[dr]\\
 179                         & *+[o][F-]{s_0}\ar@/_/[d]_a\\
 180                         & *+[o][F-]{s_1}\ar@/_/[u]_b\ar@/_/[d]_a\\
 181                         & *+[o][F-]{s_2}\ar@/_/[d]_a\ar@/_/[u]_b\\
 182                         & \ldots\ar@/_/[u]_b\\
 183                 }$
 184                 $P:=\xymatrix@C=1pc@R=1pc{
 185                         \ar[dr]\\
 186                         & *+[o][F-]{s_0}\ar@/_/[d]_a\ar[r]^\tau & *+[o][F-]{s_0}\ar@(r,u)[]_b\\
 187                         & *+[o][F-]{s_1}\ar@/_/[u]_b\ar@/_/[d]_a\ar@/_/[ur]_\tau\\
 188                         & *+[o][F-]{s_2}\ar@/_/[d]_a\ar@/_/[u]_b\ar@/_1pc/[uur]_\tau\\
 189                         & \ldots\ar@/_/[u]_b\ar@/_2pc/[uuur]_\tau\\
 190                 } $
 191 \end{enumerate}
 192
 193 % 1.5
 194 \subsection{Testing equivalences}
 195
 196 \end{document}