\subsection*{1.a}
\emph{Consider the train gate controller example of slide 9, lecture
\emph{Timed Automata}. Give an example of a series of timed transitions
(including intermediate states) of the composed system (so the product
construction of the three automata) showing a train approaching and finally
leaving the gate.}
\begin{figure}[ht]
	\centering
	\includegraphics[width=.3\linewidth]{1a}
	\caption{Timed transitions of the composed system}
\end{figure}

\subsection*{1.b}
\emph{Consider the timed automaton in figure 1 of the paper ”Timed Automata” by
Rajeev Alur. Suppose initially we have a zone $(s0, [0\leq x\leq 4, 0\leq y
\leq 3])$. Give the zone after a sequence a.b and show the intermediate steps
in the derivation.}

We define:\\
$e_0=\langle s_0, a, \emptyset, [x:=0] s_1\rangle$ and\\
$e_1=\langle s_1, a, \emptyset, [y:=0] s_2\rangle$\\

And we derive:\\
\scalebox{.99}{\parbox{.5\linewidth}{%
	\begin{align*}
		succ(e_1, succ(e_0, [0\leq x\leq 4, 0\leq y])) =&
			succ(e_1, ((([0\leq x\leq 4, 0\leq y]\wedge\emptyset)\Uparrow)
				\wedge\emptyset\wedge [x<1])[x:=0])\\
		=& succ(e_1, (([0\leq x\leq 4, 0\leq y]\Uparrow)
			\wedge\emptyset\wedge [x<1])[x:=0])\\
		=& succ(e_1, [0\leq x<1, 0\leq y][x:=0])\\
		=& succ(e_1, [x=0, 0\leq y])\\
		=& ((([x=0, 0\leq y]\wedge [x<1])\Uparrow)
			\wedge [x<1]\wedge [x<1])[y:=0]\\
		=& (([0\leq x<1, 0\leq y]\Uparrow)\wedge [x<1]\wedge [x<1])[y:=0]\\
		=& [0\leq x<1, y=0]\\
	\end{align*}}}

\subsection*{1.c}
\emph{Consider the timed automaton in figure 1 of the paper \emph{Timed
Automata} by Rajeev Alur. Give the zone automaton of the timed automaton, with
initial state $(s0, [x = 0, y = 0])$.}
\begin{figure}[ht]
	\centering
	\includegraphics[width=.7\linewidth]{1c}
	\caption{Zone automaton}
\end{figure}

