## 5 Reachability Checking
### Timed Model  
For a given TIS, let the symbol \(S=\prod_{\mathbf{i}\in\mathcal{A},\mathcal{U}\in\left(L_{\mathbf{i}}\times\mathbb{R} _{+}^{|\mathbf{X}_{\mathbf{i}}|}\right)}\) denote the non-empty set of all the _global states_. Furthermore, for a specific global state \(s=((\ell_{1},v_{1}),\ldots,(\ell_{n},v_{n}),(\ell_{\mathcal{E}},v_{\mathcal{E }}))\in S\), let the symbols \(l_{\mathbf{i}}(s)=\ell_{1}\) and \(v_{\mathbf{i}}(s)=v_{\mathbf{i}}\) represent, respectively, the local component and the clock valuation of the agent \(\mathbf{i}\in\mathcal{A}\cup\mathcal{E}\) in the global state \(s\). We define a _timed model_ (or simply a _model_) for a given TIS as a tuple \(\mathcal{M}=(Act,S,\iota,T,\mathcal{V})\), where: \(\iota=\prod_{\mathbf{i}\in\mathcal{A},\mathcal{U}\in\left(L_{\mathbf{i}} \times\mathbb{R}_{+}^{|\mathbf{X}_{\mathbf{i}}|}\right)}\) is the set of all _initial_ global states; \(\mathcal{V}(s)=\bigcup_{\mathbf{i}\in\mathcal{A},\mathcal{U}\in\mathcal{V}} \mathcal{V}_{\mathbf{i}}(l_{\mathbf{i}}(s))\); \(T\subseteq S\times\left(Act\cup\mathbb{R}_{+}\right)\times S\) is a transition relation defined by action and time transitions. This relation is crucial in understanding how the system evolves, as it captures the possible transitions from one global state to another based on actions and time. For an action \(\widetilde{a}\in Act\), an action transition \((s,\widetilde{a},s^{\prime})\in T\) (denoted as \(s\stackrel{{\widetilde{a}}}{{\rightarrow}}s^{\prime}\)) holds if, for all \(\mathbf{i}\in\mathcal{A}\cup\mathcal{E}\), there exists a local transition \(t_{\mathbf{i}}(l_{\mathbf{i}}(s),l_{\mathcal{E}}(s),\alpha_{\mathbf{i}}, \mathbb{X}^{\prime},\widetilde{a})=l_{\mathbf{i}}(s^{\prime})\) such that \(v_{\mathbf{i}}(s)\models\alpha_{\mathbf{i}}\) and \(v_{\mathbf{i}}^{\prime}(s^{\prime})=v_{\mathbf{i}}(s)[\mathbb{X}^{\prime}:=0]\). Additionally, there must exist a local transition \(t_{\mathcal{E}}(l_{\mathcal{E}}(s),\alpha_{\mathcal{E}},\mathbb{X}^{\prime}, \widetilde{a})=l_{\mathcal{E}}(s^{\prime})\) such that \(v_{\mathcal{E}}(s)\models\alpha_{\mathcal{E}}\) and \(v_{\mathcal{E}}^{\prime}(s^{\prime})=v_{\mathcal{E}}(s)[\mathbb{X}^{\prime}:=0]\). A time transition \((s,\delta,s^{\prime})\in T\) holds if, for all \(\mathbf{i}\in\mathcal{A}\cup\mathcal{E}\), we have \(l_{\mathbf{i}}(s)=l_{\mathbf{i}}(s^{\prime})\) and \(v_{\mathbf{i}}^{\prime}(s^{\prime})=v_{\mathbf{i}}(s)+\delta\), where \(\delta\in\mathbb{R}_{+}\). An infinite _path_\(\pi\) in \(\mathcal{M}\) is defined as a sequence \(\pi=(s_{0},s_{1},\ldots)\) of states such that \(s_{0}\) is an initial state, and for each even \(i\geq 0\), there exists \(\delta\in\mathbb{R}_{+}\) such that \((s_{i},\delta,s_{i+1})\in T\). For each odd \(i>0\), there exists a joint action \(\widetilde{a}\) such that \((s_{i},\widetilde{a},s_{i+1})\in T\). Note that the above definition of a path ensures that the first transition is a time transition. Each action transition is followed by a time transition, and each time transition is followed by an action transition. Semantics in which every action transition is preceded by a time transition with \(\delta>0\) is strongly monotonic. Strongly monotonic semantics require that no two events occur at the same time. The transition system (timed model) \(\mathcal{M}\) of a timed interpreted system typically has infinitely many states and infinitely many labels. However, the reachability problem for \(\mathcal{M}\) can be reduced to a reachability problem for a transition system with finitely many states and finitely many labels. Let \(c_{max}\) be the largest constant \(c\) such that some clock \(x\) is compared with \(c\) in some constraint appearing in a guard of TIS. By \(\hat{\mathcal{M}}\), we denote the transition system for a timed interpreted system that differs from \(\mathcal{M}\) only in its set of labels: for the set of labels of \(\hat{\mathcal{M}}\), we take the set \(\mathcal{V}\cup[0,c_{max}+1]\).