2 \emph{Consider the train gate controller example of slide
9, lecture
3 \emph{Timed Automata
}. Give an example of a series of timed transitions
4 (including intermediate states) of the composed system (so the product
5 construction of the three automata) showing a train approaching and finally
9 \includegraphics[width=
.3\linewidth]{1a
}
10 \caption{Timed transitions of the composed system
}
14 \emph{Consider the timed automaton in figure
1 of the paper ”Timed Automata” by
15 Rajeev Alur. Suppose initially we have a zone $(s0,
[0\leq x
\leq 4,
0\leq y
16 \leq 3])$. Give the zone after a sequence a.b and show the intermediate steps
20 $e_0=
\langle s_0, a,
\emptyset,
[x:=
0] s_1
\rangle$ and\\
21 $e_1=
\langle s_1, a,
\emptyset,
[y:=
0] s_2
\rangle$\\
24 \scalebox{.99}{\parbox{.5\linewidth}{%
26 succ(e_1, succ(e_0,
[0\leq x
\leq 4,
0\leq y
])) =&
27 succ(e_1, (((
[0\leq x
\leq 4,
0\leq y
]\wedge\emptyset)
\Uparrow)
28 \wedge\emptyset\wedge [x<
1])
[x:=
0])\\
29 =& succ(e_1, ((
[0\leq x
\leq 4,
0\leq y
]\Uparrow)
30 \wedge\emptyset\wedge [x<
1])
[x:=
0])\\
31 =& succ(e_1,
[0\leq x<
1,
0\leq y
][x:=
0])\\
32 =& succ(e_1,
[x=
0,
0\leq y
])\\
33 =& (((
[x=
0,
0\leq y
]\wedge [x<
1])
\Uparrow)
34 \wedge [x<
1]\wedge [x<
1])
[y:=
0]\\
35 =& ((
[0\leq x<
1,
0\leq y
]\Uparrow)
\wedge [x<
1]\wedge [x<
1])
[y:=
0]\\
40 \emph{Consider the timed automaton in figure
1 of the paper
\emph{Timed
41 Automata
} by Rajeev Alur. Give the zone automaton of the timed automaton, with
42 initial state $(s0,
[x =
0, y =
0])$.
}
45 \includegraphics[width=
.7\linewidth]{1c
}
46 \caption{Zone automaton
}