8efa2966d4c8595656c2ac1c985bac2fd66a53d6
[tt1516.git] / 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 & 0 & 0\cr
101 P_3 & 0 & 0 & 1 & 0\cr
102 P_4 & 0 & 0 & 1 & 1\cr
103 }$
104 \item
105 $P_1=\xymatrix@C=1pc@R=1pc{
106 \ar[dr]&\\
107 & *+[o][F-]{s_0}\ar[d]^a\\
108 & *+[o][F-]{s_1}\ar[d]^b\\
109 & *+[o][F-]{s_2}\ar[d]^c\\
110 & *+[o][F-]{s_3}\\
111 }$
112 $P_2=\xymatrix@C=1pc@R=1pc{
113 \ar[dr]&\\
114 & *+[o][F-]{s_0}\ar[d]^a\\
115 & *+[o][F-]{s_1}\ar[d]^b\\
116 & *+[o][F-]{s_2}\ar[dl]_c\ar[dr]^d\\
117 *+[o][F-]{s_3} & & *+[o][F-]{s_4}\\
118 }$
119 $P_3=\xymatrix@C=1pc@R=1pc{
120 \ar[dr] &\\
121 & *+[o][F-]{s_0}\ar[d]^a\\
122 & *+[o][F-]{s_1}\ar[dl]_b\ar[dr]^b\\
123 *+[o][F-]{s_2}\ar[d]^c & & *+[o][F-]{s_3}\ar[d]^d\\
124 *+[o][F-]{s_4} & & *+[o][F-]{s_5}\\
125 }$
126 $P_4=\xymatrix@C=1pc@R=1pc{
127 \ar[dr] &\\
128 & *+[o][F-]{s_0}\ar[dl]_a\ar[dr]^a\\
129 *+[o][F-]{s_2}\ar[d]^b & & *+[o][F-]{s_3}\ar[d]^b\\
130 *+[o][F-]{s_4}\ar[d]^c & & *+[o][F-]{s_5}\ar[d]^d\\
131 *+[o][F-]{s_6} & & *+[o][F-]{s_7}
132 }$
133 \end{enumerate}
134
135 \subsection{Testing equivalences}
136 \begin{enumerate}[a)]
137 \item
138 \begin{align*}
139 \sigma\in traces(p)\leftrightarrow
140 p\text{ \bf after }\sigma\text{ \bf refuses }\emptyset\\
141 \sigma\in traces(p)\leftrightarrow
142 \exists p':p\overset{\sigma}{\Rightarrow}p'\text{ and }\forall a\in
143 \emptyset:p'\cancel{\overset{a}{\rightarrow}} & & 2.\\
144 \sigma\in traces(p)\leftrightarrow
145 \exists p':p\overset{\sigma}{\Rightarrow}p'\\
146 \sigma\in \{\sigma\in L^*|p\overset{\sigma}{\Rightarrow}\}\leftrightarrow
147 \exists p':p\overset{\sigma}{\Rightarrow}p'& & \square\\
148 \end{align*}
149 \item
150 \begin{align*}
151 p\text{ \bf after }\sigma\text{ \bf refuses } A\leftrightarrow
152 \sigma\cdot A\in Ftraces(p)\\
153 \exists p':p\overset{\sigma}{\Rightarrow}p'\text{ and }\forall a\in
154 A:p'\cancel{\overset{a}{\rightarrow}} \leftrightarrow
155 \sigma\cdot A\in Ftraces(p) & & 2.\\
156 \exists p':p\overset{\sigma}{\Rightarrow}p'\text{ and }\forall a\in
157 A:p'\cancel{\overset{a}{\rightarrow}} \leftrightarrow
158 \sigma\cdot A\in \{\psi\in(L\cup
159 \mathcal{P}(L))^*|p\overset{\sigma}{\Rightarrow}\} & & 4.\\
160 \end{align*}
161 \item
162 \begin{align*}
163 \end{align*}
164 \item
165 \begin{align*}
166 \end{align*}
167 \end{enumerate}
168
169 \subsection{Testing equivalences}
170 \subsection{Testing equivalences}
171
172 \end{document}