## 2 Dense-Timed Deontic Interpreted System
### An Example of a Real-Time MAS and Its DTDIS Model
#### Semantics of EMTLKD
Let \(M\) be the dense-timed deontic model of the FTTCS, \(\varphi=F_{[0,14)}(tunnel_{1}\wedge tunnel_{2})\) be an EMTLKD formula, and \(\rho\) be a run with the following prefix:_\[M,\lambda_{\rho}[n] \
ot\models f,\]4 \[M,\lambda_{\rho}[n] \
ot\models f,\]5 \[M,\lambda_{\rho}[n] \
ot\models f,\]6 \[M,\lambda_{\rho}[n] \
ot\models f,\]7 \[M,\lambda_{\rho}[n] \
ot\models f,\]8 \[M,\lambda_{\rho}[n] \
ot\models f,\]9 \[M,\lambda_{\rho}[n] \models p\text{ iff }p\in\mathcal{V}(\lambda_{\rho}[n]),\]0 \[M,\lambda_{\rho}[n] \models p\text{ iff }p\in\mathcal{V}(\lambda_{\rho}[n]),\]1  
_The corresponding path \(\lambda_{\rho}=\lambda_{\rho}[0],\lambda_{\rho}[1],\lambda_{\rho}[2],\lambda_{ \rho}[3],\lambda_{\rho}[4],\ldots\) takes the following form:_  
\[M,\lambda_{\rho}[n] \models p\text{ iff }p\in\mathcal{V}(\lambda_{\rho}[n]),\]2 \[M,\lambda_{\rho}[n] \models p\text{ iff }p\in\mathcal{V}(\lambda_{\rho}[n]),\]3 \[M,\lambda_{\rho}[n] \models p\text{ iff }p\in\mathcal{V}(\lambda_{\rho}[n]),\]4 \[M,\lambda_{\rho}[n] \models p\text{ iff }p\in\mathcal{V}(\lambda_{\rho}[n]),\]5 \[M,\lambda_{\rho}[n] \models p\text{ iff }p\in\mathcal{V}(\lambda_{\rho}[n]),\]6 \[M,\lambda_{\rho}[n] \models p\text{ iff }p\in\mathcal{V}(\lambda_{\rho}[n]),\]7 \[M,\lambda_{\rho}[n] \models p\text{ iff }p\in\mathcal{V}(\lambda_{\rho}[n]),\]8 \[M,\lambda_{\rho}[n] \models p\text{ iff }p\in\mathcal{V}(\lambda_{\rho}[n]),\]9 \[M,\lambda_{\rho}[n] \models\
eg p\text{ iff }p\
ot\in\mathcal{V}(\lambda_{\rho}[n]),\]0 \[M,\lambda_{\rho}[n] \models\
eg p\text{ iff }p\
ot\in\mathcal{V}(\lambda_{\rho}[n]),\]1 \[M,\lambda_{\rho}[n] \models\
eg p\text{ iff }p\
ot\in\mathcal{V}(\lambda_{\rho}[n]),\]2 \[M,\lambda_{\rho}[n] \models\
eg p\text{ iff }p\
ot\in\mathcal{V}(\lambda_{\rho}[n]),\]3 \[M,\lambda_{\rho}[n] \models\
eg p\text{ iff }p\
ot\in\mathcal{V}(\lambda_{\rho}[n]),\]4 \[M,\lambda_{\rho}[n] \models\
eg p\text{ iff }p\
ot\in\mathcal{V}(\lambda_{\rho}[n]),\]5 \[M,\lambda_{\rho}[n] \models\
eg p\text{ iff }p\
ot\in\mathcal{V}(\lambda_{\rho}[n]),\]6  
_Observe that \(tunnel_{1}\) and \(tunnel_{2}\) are both true at position \(\lambda_{\rho}[14]\). Hence, we have \(M,\lambda_{\rho}[14]\models tunnel_{1}\wedge tunnel_{2}\). This implies that \(M,\lambda_{\rho}[0]\models F_{[0,14)}(tunnel_{1}\wedge tunnel_{2})\) holds._  
Identifying the existential validity of an EMTLKD formula \(\varphi\) within a dense-timed deontic model \(M\) constitutes an _existential model checking problem_. Put differently, this problem seeks to ascertain whether \(M\models\varphi\). One of the key challenges in verifying EMTLKD properties is the increasing computational complexity as the number of agents and their interactions grow. In multi-agent systems, the state-space explosion problem arises not only from the large number of agents but also from the complexity of their local states. Each agent's local state in a DTDIS must maintain not only a discrete execution state (determined by past actions) but also the values of real-time clocks, which evolve continuously. This combination of discrete and dense-time information significantly increases the number of possible system states, making exhaustive verification computationally expensive. To address this issue, one effective approach is to first translate EMTLKD into its corresponding linear temporal logic with epistemic and deontic components, \(\mathrm{ELTLKD_{q}}\). This transformation simplifies the structure of the logic by removing some of the branching aspects of temporal logic, while still preserving key epistemic, temporal, and deontic properties of the system. Additionally, this representation allows us to apply bounded model checking (BMC), which enables verification within a finite scope, mitigating the impact of state-space explosion. Bounded model checking works by limiting the exploration to a finite, pre-specified number of steps or time units, and then searching for counterexamples to the given properties within this bound.