1b misschien
[mc1516the.git] / first.tex
1 \subsection*{1.a}
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
6 leaving the gate.}
7 \begin{figure}[h]
8 \centering
9 \includegraphics[width=.3\linewidth]{1a}
10 \caption{Timed transitions of the composed system}
11 \end{figure}
12
13 \subsection*{1.b}
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
17 in the derivation.}
18
19 We define:\\
20 $e_0=\langle s_0, a, [], [x:=0] s_1\rangle$ and\\
21 $e_1=\langle s_1, a, [], [y:=0] s_2\rangle$\\
22
23 And we derive:\\
24 \begin{align*}
25 succ(e_1, succ(e_0, [0\leq x\leq 4, 0\leq y])) =&
26 succ(e_1, ((([0\leq x\leq 4, 0\leq y]\wedge [])\Uparrow)\wedge []\wedge [x<1])[x:=0])\\
27 =& succ(e_1, (([0\leq x\leq 4, 0\leq y]\Uparrow)\wedge []\wedge [x<1])[x:=0])\\
28 =& succ(e_1, ([0\leq x<1, 0\leq y])[x:=0])\\
29 =& succ(e_1, [x=1, 0\leq y][x:=0])\\
30 =& ((([x=1, 0\leq y]\wedge [x<1])\Uparrow)\wedge [x<1]\wedge [x<1])[y:=0]\\
31 =& (([x=1, 0\leq y]\Uparrow)\wedge [x<1]\wedge [x<1])[y:=0]\\
32 =& [x<1, y=0]
33 \end{align*}
34
35 \subsection*{1.c}
36 \emph{Consider the timed automaton in figure 1 of the paper \emph{Timed
37 Automata} by Rajeev Alur. Give the zone automaton of the timed automaton, with
38 initial state $(s0, [x = 0, y = 0])$.}