## 2 Dense-Timed Deontic Interpreted System
### An Example of a Real-Time MAS and Its DTDIS Model
Similarly, train \(T_{i}\) synchronizes with controller \(C\) on actions \(approach_{i}\), indicating the setting of \(C\) to state \(i\), as well as \(out_{i}\), representing the returning of \(C\) to state 0. Lastly, the action \(in_{i}\) denotes the entry of train \(T_{i}\) into the tunnel. For environment \(\mathcal{E}\), for the sake of clarity in presentation, we will consider only one local state: \(L_{\mathcal{E}}=\cdot\). The set of actions for \(\mathcal{E}\) is \(Act_{\mathcal{E}}=\epsilon_{\mathcal{E}}\). The local protocol of \(\mathcal{E}\) is defined as follows: \(P_{\mathcal{E}}(\cdot)=Act_{\mathcal{E}}\). The set of clocks of \(\mathcal{E}\) is empty, and the invariant function is \(\mathcal{I}_{\mathcal{E}}(\cdot)=\emptyset\)  
From Figure 1, we can easily derive the local evolution functions of each agent. As an example, we provide the definition of the local evolution function for train \(T_{1}\). The remaining definitions follow similarly. Let \(state\) denote a local state of train \(T_{1}\), and \(Act=\prod_{i=1}^{n}Act_{T_{i}}\times Act_{\mathcal{C}}\times Act_{\mathcal{E}}\), with \(Act_{T_{i}}=\{start_{i},approach_{i},out_{i},in_{i},e_{T_{i}}\}\), \(Act_{\mathcal{C}}=\{start_{i},approach_{i},out_{i},in_{i},error_{i}\), \(repair_{i},e_{C}\mid i=1,..,n\}\), and \(Act_{\mathcal{E}}=\{\epsilon_{\mathcal{E}}\}\). Moreover, let \(\overline{a}\in Act\), \(act_{T_{i}}(\overline{a})\), \(act_{C}(\overline{a})\), and \(act_{\mathcal{E}}(\overline{a})\), respectively, denote an action of the \(i-\)th train, the controller, and the environment. The local evaluation function of train \(T_{1}\) is the following:  
* \(t_{T_{1}}(state,\cdot,true,\emptyset,\overline{a})=state\), if \(\overline{a}\
eq\overline{e}\) and \(act_{T_{1}}(\overline{a})=e_{T_{1}}\). * \(t_{T_{1}}(away,\cdot,true,\{x_{1}\},\overline{a})=try\), if \(act_{T_{1}}(\overline{a})=act_{C}(\overline{a})=Start_{1}\). * \(t_{T_{1}}(try,\cdot,x_{1}<\Delta,\{x_{1}\},\overline{a})=wait\), if \(act_{T_{1}}(\overline{a})=act_{C}(\overline{a})=approach_{1}\). * \(t_{T_{1}}(wait,\cdot,x_{1}>\delta,\emptyset,\overline{a})=tunnel\), if \(act_{T_{1}}(\overline{a})=act_{C}(\overline{a})=in_{1}\). * \(t_{T_{1}}(tunnel,\cdot,true,\emptyset,\overline{a})=away\), if \(act_{T_{1}}(\overline{a})=act_{C}(\overline{a})=out_{1}\). We can define the set of possible global states \(S\) for the scenario as the product \(\prod_{i=1}^{n}(L_{T_{i}}\times\mathbb{R})\times L_{\mathcal{C}}\times L_{ \mathcal{E}}\), and we consider the following set of initial states \(\iota=\{s^{0}\}\), where \(s^{0}=((\text{away},0),\ldots,(\text{away},0),0,\cdot)\). The example can be scaled by adding trains or adjusting the time-delay constants \(\delta\) and \(\Delta\). It is important to note that the maintenance of the mutual exclusion property (i.e., ensuring that no two trains are in the tunnel simultaneously) relies on the relative values of the time-delay constants \(\delta\) and \(\Delta\). However, the correctness of the protocol, ensured by appropriate settings of the constants \(\delta\) and \(\Delta\) (i.e., \(\delta>\Delta\)), can be compromised if, for unknown reasons, the controller ceases to function and transitions to the \"faulty\" state. It should be straightforward to deduce the dense-timed deontic model induced by the above description of the FTCS scenario. In the dense-timed deontic model of the scenario, we assume the following set of proposition variables, \(\mathcal{PV}=\{tunnel_{i}\mid i=1,\ldots,n\}\cup\{faulty\}\), and the following definition of valuation functions for trains, \(\mathcal{V}_{T_{i}}(tunnel)=tunnel_{i}\), for \(i=1,\ldots,n\), and the controller \(C\), \(\mathcal{V}_{C}(F)=faulty\).