## 3 Timed Interpreted Systems
### TIS Formalism  
We begin by establishing some notation that will be used throughout the paper. Let \(\mathbb{R}_{+}\) denote the set of positive real numbers, \(\mathbb{N}\) denote the set of natural numbers, and \(\mathbb{X}\) denote a finite set of variables known as clocks. Each clock is a variable that ranges over the set of non-negative real numbers. For a clock \(x\in\mathbb{X}\) and a constant \(c\in\mathbb{N}\), we define the set of clock constraints over \(\mathbb{X}\), denoted by \(\mathcal{C}(\mathbb{X})\). These constraints, \(\alpha\)c, are conjunctions of comparisons between a clock and a time constant \(c\) taken from the set of natural numbers, \(\mathbb{N}\). Next, we recall the TIS definition from [4]. Let \(\mathcal{A}=\mathbf{i}_{1},\ldots,\mathbf{i}_{n}\) represent a non-empty finite set of agents, and let \(\mathcal{E}\) represent a special agent used to model the environment in which these agents operate. Additionally, let \(\mathcal{AP}=\bigcup_{i\in\mathcal{A},\cup\mathcal{E}}\mathcal{AP}_{i}\) be the set of propositional variables, where \(\mathcal{AP}_{i}\bigcap\mathcal{AP}_{i}=\emptyset\) for all distinct agents \(\mathbf{i},\mathbf{j}\in\mathcal{A}\cup\mathcal{E}\). The set of agents, \(\mathcal{A}\), and the environment, \(\mathcal{E}\), form a multi-agent system. A _timed interpreted system_ is defined as a tuple:  
\[\text{TIS}=(\{L_{i},\mathit{Act}_{i},\mathbb{X}_{i},\mathbb{P}_{i},\mathcal{ V}_{i},\mathbf{i}_{i}\}_{i\in\mathcal{A}\cup\{\mathcal{E}\}},\{t_{i}\}_{i\in \mathcal{A}},\{t_{\mathcal{E}}\}),\]where \(L_{\mathbf{i}}\) is a non-empty set of _locations_ for an agent \(\mathbf{i}\), and \(\iota_{\mathbf{i}}\subseteq L_{\mathbf{i}}\) is a non-empty set of initial locations. The set \(Act_{\mathbf{i}}\) represents the _possible actions_ that the agent \(\mathbf{i}\) can perform. Each agent has a special action, referred to as the 'null' or'silent' action, denoted as \(\epsilon_{\mathbf{i}}\), which belongs to \(Act_{\mathbf{i}}\), and similarly, \(\epsilon_{\mathcal{E}}\) belongs to \(Act_{\mathcal{E}}\). The set \(\mathbb{X}_{\mathbf{i}}\) denotes a non-empty set of _clocks_, ensuring that \(\mathbb{X}_{\mathbf{i}}\cap\mathbb{X}_{\mathbf{j}}=\emptyset\) for all distinct agents \(\mathbf{i},\mathbf{j}\in\mathcal{A}\cup\mathcal{E}\). The function \(P_{\mathbf{i}}:L_{\mathbf{i}}\to 2^{Act_{\mathbf{i}}}\) is a _protocol function_ that models the program executed by the agent \(\mathbf{i}\). Formally, for any agent \(\mathbf{i}\in\mathcal{A}\cup\mathcal{E}\), the actions are determined according to this local protocol. A _valuation function_\(\mathcal{V}_{\mathbf{i}}:L_{\mathbf{i}}\to 2^{\mathcal{AP}_{\mathbf{i}}}\) assigns to each location a set of atomic formulae that are considered true at that location. The set \(Act=Act_{1}\times\ldots\times Act_{n}\times Act_{\mathcal{E}}\) represents the collection of _joint actions_ performed by all agents. The evolution function specifies how local states 'evolve' based on several factors: the local state of the agent, the actions of other agents, the local state of a special agent representing the environment, the clock constraints of the agent \(\mathbf{i}\), and the set of clocks to reset. A function \(t_{\mathbf{i}}:L_{\mathbf{i}}\times L_{\mathcal{E}}\times\mathcal{C}(\mathbb{ X}_{\mathbf{i}})\times 2^{\mathbb{X}_{\mathbf{i}}}\times Act\to L_{ \mathbf{i}}\) is a (partial) _evolution function_ for agents, while a function \(t_{\mathcal{E}}:L_{\mathcal{E}}\times\mathcal{C}(\mathbb{X}_{\mathcal{E}}) \times 2^{\mathbb{X}_{\mathcal{E}}}\times Act\to L_{\mathcal{E}}\) is a (partial) _evolution function_ for the environment. We assume that the environment's locations, actions, and clocks are 'public', while the locations and clocks of any agent are considered 'private'.