4 \section{Theory of Labelled Transition Systems
}
5 \subsection{Testing equivalences
}
8 ~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5
\cr
12 Q_4 &
0 &
0 &
0 &
1\cr
13 Q_5 &
0 &
0 &
0 &
0 &
1\cr
16 ~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5
\cr
20 Q_4 &
0 &
1 &
1 &
1\cr
21 Q_5 &
0 &
1 &
1 &
1 &
1\cr
24 ~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5
\cr
28 Q_4 &
0 &
1 &
1 &
1\cr
29 Q_5 &
0 &
1 &
1 &
1 &
1\cr
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$.
41 ~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5
\cr
45 Q_4 &
0 &
1 &
1 &
1\cr
46 Q_5 &
0 &
1 &
1 &
1 &
1\cr
50 ~ & Q_1 & Q_2 & Q_3 & Q_4 & Q_5
\cr
54 Q_4 &
0 &
0 &
0 &
1\cr
55 Q_5 &
0 &
0 &
0 &
1 &
1\cr
57 \item All processes as explained in $d)$.
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
68 \subsection{Testing equivalences
}
71 ~ & P_1 & P_2 & P_3 & P_4
\cr
75 P_4 &
0 &
0 &
0 &
1\cr
78 ~ & P_1 & P_2 & P_3 & P_4
\cr
82 P_4 &
0 &
1 &
1 &
1\cr
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$.
90 ~ & P_1 & P_2 & P_3 & P_4
\cr
94 P_4 &
0 &
0 &
1 &
1\cr
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
105 $P_1=
\xymatrix@C=
1pc@R=
1pc
{
107 & *+
[o
][F-
]{s_0
}\ar[d
]^a\\
108 & *+
[o
][F-
]{s_1
}\ar[d
]^b\\
109 & *+
[o
][F-
]{s_2
}\ar[d
]^c\\
112 $P_2=
\xymatrix@C=
1pc@R=
1pc
{
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
}\\
119 $P_3=
\xymatrix@C=
1pc@R=
1pc
{
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
}\\
126 $P_4=
\xymatrix@C=
1pc@R=
1pc
{
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
}
135 \subsection{Testing equivalences
}
136 \begin{enumerate
}[a)
]
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\\
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.\\
169 \subsection{Testing equivalences
}
170 \subsection{Testing equivalences
}