## 2 Background of Timed Automata  
Firstly, some related definitions for timed automata [1] are given. Let \(C\) be a set of clocks, and \(\Phi(C)\) be a set of clock constraints. A clock constraint is defined as follows: \(\delta:=\textit{true}\mid x\sim n\mid\delta_{1}\wedge\delta_{2}\mid-\delta_{1}\), where \(\sim\in\{=,\leq,\geq,<,>\}\), where \(x\) is a clock in \(C\) and \(n\) is a non-negative integer. The set of downward constraints obtained with \(\sim\in\{\leq,<\}\) is denoted as \(\Phi_{\leq,<}(C)\). A clock valuation \(v\) for a set of clocks \(C\) is a function which assigns a real value to each clock. If the clock valuation \(v\) makes the clock constraint \(\delta\) true, then \(v\) satisfies \(\delta\) based on \(C(v\mid=\delta)\). For any \(d\in R^{+}\), let \(v+d\) denote the clock valuation \(v^{\prime}\) such that \(v^{\prime}(c)=v(c)+d\) for all \(c\in C\). For a set of clocks \(X\subseteq C\), let the clock resetting notion \([X\mapsto 0]v\) denote the valuation \(v^{\prime}\) such that \(v^{\prime}(c)=v(c)\) for any \(c\in C\wedge c\
ot\in X\) and \(v^{\prime}(x)=0\) for all \(x\in X\). **Definition 1** (Timed Automata). : _A Timed Automaton is a tuple \(A=(S,Init,\Sigma,C,L,T)\), where \(S\) is a finite set of states; \(Init\subseteq S\) is a set of initial states; \(\Sigma\) is a set of events; \(C\) is a finite set of clocks; \(L:S\rightarrow\Phi_{\leq<}(C)\) is a function that gives a state invariant \(\Phi_{\leq,<}(C)\) to each state; and \(T\subseteq S\times\Sigma\times\Phi(C)\times 2^{C}\times S\) is a transition with a set of clock constraints \(\Phi(C)\)._  
Based on the concrete semantics, the Timed Automaton \(A\) is a transition system. Each node is a pair \((s,v)\), where \(s\in S\) is a state and \(v\) is a clock valuation which satisfies \(v\mid=L(s)\). A run of \(A\) is a finite sequence \(\bigtriangleup=\langle(s_{0},v_{0}),(d_{0},e_{0}),(s_{1},v_{1}),(d_{1},e_{1}),\cdots,(s_{i},v_{i}),(d_{i},e_{i}),\cdots\rangle\), where \(s_{0}\inInit;v_{0}\) resets each clock to zero; for all \(i\geq 0\), there is a transition \((s_{i},e_{i},\delta,X,s_{i+1})\)\(\in T\), such that \(v_{i}+d_{i}\mid=L(s_{i})\), \(v_{i}+d_{i}\mid=\delta\), \(v_{i+1}=[X\mapsto 0](v_{i}+d_{i})\) and \(v_{i+1}\mid=L(s_{i+1})\). Given a run \(\bigtriangleup\), we can get its timed language \(\langle(d_{0},e_{0}),(d_{1},e_{1}),\cdots,(d_{i},e_{i}),\cdots\rangle\). We use \(\mathit{Lan}(A)\) to denote all the languages of \(A\). If the languages of two timed automata are the same, they are equivalent. Due to the infinity of time, the Timed Automaton \(A\) is essentially a transition system with infinite nodes. To make the verification possible, it must be transformed into a graph with finite transitions. The most commonly used abstraction technique is the zone abstraction. We can obtain a zone graph with finite nodes after zone abstraction. A zone is a linear inequality or a conjunction of linear inequalities defined on \(C\), such as \(x-y\leq 5\), \(y>3\wedge x<7\), etc., where \(x,y\in C\). Given a zone \(\delta\), let \(\delta^{\dagger}\) denote the zone obtained from \(\delta\) by delaying any time. **Definition 2** (Zone Graph). : _Given a Timed Automaton \(A=(S,Init,\Sigma,C,L,T)\), the zone graph \(ZG(A)\) is a tuple \((S_{z},Init_{z},\Sigma,T_{z})\), such that \(S_{z}\) denotes a set of nodes \((s,\delta)\) where \(s\in S\) and \(\delta\) is a clock constraint; \(Init_{z}=\{(init,(\wedge_{c\in C}c=0)^{\dagger}\wedge L(init))\mid init\in Init\}\) is a set of initial nodes; \(T_{z}:S_{z}\times\Sigma\times S_{z}\) is a transition relation such that \(((s_{1},\delta_{1}),e,(s_{2},\delta_{2}))\in T_{z}\) iff \((s_{1},e,\delta,X,s_{2})\in T\), \(\delta_{1}\wedge\delta\) is not empty, \([X\mapsto 0](\delta_{1}\wedge\delta)\wedge L(s_{2})\) is not empty and \(\delta_{2}=D(([X\mapsto 0](\delta_{1}\wedge\delta))^{\dagger}\wedge L(s_{2}))\). (\(D\) is a normalization function [1])._  
Figure 1 shows a Timed Automaton example which is a switch, where the initial state is _Off_.