## 5 Reachability Checking
### Reachability Analysis  
The reachability problem for multi-agent systems modelled by Timed Interpreted Systems involves determining whether, for a specified set of target locations, a state containing a target location can be reached from some initial state. We assume that a propositional formula representing a particular property describes the set of target locations. To verify the reachability of a state that satisfies this property using the Bounded Model Checking method, the model's transition relation is initially unfolded iteratively to a certain depth \(k\) and encoded as a quantifier-free first-order formula of state variables. Subsequently, the property is converted into a quantifier-free first-order formula of state variables, and an SMT-solver is used to check the satisfiability of the conjunction of these two formulae. If the conjunction (denoted in the algorithm by \(\beta_{k}\)) is satisfiable, it can be concluded that a path to a target location has been found. If not, the value of \(k\) is incremented by 2, as time transitions do not alter the global locations (Algorithm 1). The parameter \(n\), which represents the number of steps in a given protocol, is crucial in determining the depth of the model's transition relation that needs to be unfolded. The SMT encoding of the reachability problem for TIS builds upon the encoding described in [49]. However, we have:  
* refined the definitions for the encoding of the transition relation (as the definition in the cited paper lacked precision), and
* incorporated real-time aspects of multi-agent systems, whereas the previous SMT encoding was limited to discrete time. Let \(\hat{\mathcal{M}}\) be a model. To formulate and solve the reachability problem for TISs, we must define the unfolding of the transition relation up to depth \(k\in\mathbb{N}\). To this end, we define a \(k\)-path as a finite prefix of a path. Note that an arbitrary state \(s\) is reachable in \(\hat{\mathcal{M}}\) if and only if it is reachable on a \(k\)-path for some \(k\geq 0\). Next, we define the formula \(\mathit{path}_{k}(\overline{\mathbf{w}}_{0},\ldots,\overline{\mathbf{w}}_{k})\), which symbolically encodes all the \(k\)-paths starting at the initial state of \(\hat{\mathcal{M}}\). The definition of the formula \(\mathit{path}_{k}(\overline{\mathbf{w}}_{0},\ldots,\overline{\mathbf{w}}_{k})\) assumes that each global state \(s\in S\) of \(\hat{\mathcal{M}}\) can be represented by a valuation of a symbolic state \(\overline{\mathbf{w}}=((w1,v_{1}),\ldots,(w_{n},v_{n}),(w_{\mathcal{E}},v_{ \mathcal{E}}))\) that consists of symbolic local states. Each symbolic local state is a pair \((w_{i},v_{i})\) of individual variables ranging over the natural numbers, which represent the local state of the agent \(\mathbf{i}\) and a clock valuation. Similarly, each action can be represented by a valuation of a symbolic joint action \(\overline{\mathbf{a}}\), which is a vector of individual variables ranging over natural numbers. Let \(\overline{\mathbf{w}}\) and \(\overline{\mathbf{w}}^{\prime}\) be two symbolic states, \(\overline{\mathbf{a}}\) a symbolic action, and \(\mathbf{d}\) a symbolic non-negative real number. We define the following quantifier-free first-order formulae:  
* \(I_{s}(\overline{\mathbf{w}})\) encodes the state \(s\) of the model \(\hat{\mathcal{M}}\),
* \(\mathcal{T}_{\sigma}(w_{i},\overline{\mathbf{a}},w^{\prime})\) encodes an action transition and ensures that every local action \(a_{i}\) in \(\overline{\mathbf{a}}\) is performed by each agent in which this action appears,
* \(\mathcal{T}_{\tau}(w_{i},\mathbf{d},w^{\prime}{}_{i})\) encodes a time transition in \(\hat{\mathcal{M}}\). For every even \(k\in\mathcal{N}\), we can now define the formula \(\mathit{path}_{k}(\overline{\mathbf{w}}_{0},\ldots,\overline{\mathbf{w}}_{k})\) as follows:  
\[\bigvee_{s\in t}I_{s}(\overline{\mathbf{w}}_{0})\wedge\bigwedge_{ \begin{subarray}{c}j=0\\ j\bmod 2=0\end{subarray}