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}[ht]
   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, \emptyset, [x:=0] s_1\rangle$ and\\
  21 $e_1=\langle s_1, a, \emptyset, [y:=0] s_2\rangle$\\
  22
  23 And we derive:\\
  24 \scalebox{.99}{\parbox{.5\linewidth}{%
  25         \begin{align*}
  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]\\
  36                 =& [0\leq x<1, y=0]\\
  37         \end{align*}}}
  38
  39 \subsection*{1.c}
  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])$.}
  43 \begin{figure}[ht]
  44         \centering
  45         \includegraphics[width=.7\linewidth]{1c}
  46         \caption{Zone automaton}
  47 \end{figure}
  48