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 \subsection*{1.c}
  20 \emph{Consider the timed automaton in figure 1 of the paper \emph{Timed
  21 Automata} by Rajeev Alur. Give the zone automaton of the timed automaton, with
  22 initial state $(s0, [x = 0, y = 0])$.}