## 4 Translation from EMTLKD to \(\mathrm{ELTLKD_{q}}\)  
The translation of the existential model checking problem for EMTLKD into the existential model checking problem for \(\mathrm{ELTLKD_{q}}\), a language defined below and interpreted over a dense-timed deontic interpreted system, is based on the work in [7]. In that work, the translation of the existential model checking problem for \(\mathrm{EMTLK}\) to the existential model checking problem for \(\mathrm{ELTLK_{q}}\) was first introduced. The extension of this translation in the current context was motivated by the necessity to incorporate all standard epistemic and deontic operators. The inclusion of deontic operators enables modeling the correct behavior of agents, allowing us to reason not only about proper system behavior but also about scenarios where agents or the system deviate from expected norms. This semantic framework effectively captures states in which agents function correctly as well as those in which they do not. Moreover, the addition of epistemic operators, which handle a group of agents, facilitates reasoning about various types of knowledge, including common knowledge, distributed knowledge, and the knowledge possessed by every agent in a group. This enhancement strengthens the modeling of multi-agent systems, where agents' knowledge and coordination play a crucial role in determining overall system behavior. Definition 3: Let 1 be an interval as assumed in Definition 1, \(\mathcal{IV}\) the set of all intervals in \(\mathbb{R}\), and \(\mathcal{PV_{\mathcal{IV}}}=\{q_{1}\mid I\in\mathcal{IV}\}\). The formulae \(\alpha\) of \(\mathrm{ELTLKD_{q}}\) are defined inductively:  
\[\alpha:=\boldsymbol{t}\mid\boldsymbol{f}\mid\boldsymbol{p}\mid\
eg\boldsymbol {p}\mid\alpha\wedge\alpha\mid\alpha\vee\alpha\mid\alpha\text{U}\alpha\mid \text{G}\alpha\mid\overline{\text{K}}_{\text{c}}\alpha\mid\overline{\text{D }}_{\text{T}}\alpha\mid\overline{\text{E}}_{\text{F}}\alpha\mid\overline{ \text{C}}_{\text{r}}\alpha\mid\overline{\text{C}}_{\text{c}}\alpha\mid \text{K}_{\text{c}_{1}}^{\text{c}_{2}}\alpha\]  
where \(p\in\mathcal{PV}\cup\mathcal{PV_{\mathcal{IV}}}\), \(\boldsymbol{c}\in\mathbb{A}\), and \(\Gamma\subseteq\mathbb{A}\). The modal operators \(\mathrm{U}\) and \(\mathrm{G}\) are read as \"_until_\" and \"_globally_\", respectively. The derived basic modal operators for \"_eventually_\" and \"_release_\" are defined as follows: \(\alpha\stackrel{{\text{\tiny{def}}}}{{=}}\mathfrak{t}\mathrm{U}\alpha\) and \(\alpha\text{R}\beta\stackrel{{\text{\tiny{def}}}}{{=}}\beta \mathrm{U}(\beta\wedge\alpha)\vee\mathrm{G}\beta\). The epistemic operators \(\overline{\text{K}}_{\text{c}}\), \(\overline{\text{D}}_{\text{T}}\), \(\overline{\text{E}}_{\text{T}}\), \(\overline{\text{C}}_{\text{r}}\), \(\overline{\text{O}}_{\text{c}}\), and \(\underline{\text{K}}_{\text{c}_{1}}^{\text{c}_{2}}\) have the same meaning as described in Section 3. Definition 4: Let \(\alpha\) and \(\beta\) be \(\mathrm{ELTLKD_{q}}\) formulae, \(M\) the dense-timed deontic model, and \(\lambda_{\rho}\) a path. By \(\lambda_{\rho}[n]\), we denote the path \(\lambda_{\rho}\) with a designated formula evaluation position \(n\in\mathbb{N}\). The  
+++ ==ERROR: No output for this page==
satisfiability _relation_\(\models^{d}\), which indicates the truth of an \(\mathrm{ELTLKD}_{\mathrm{q}}\) formula in the model \(M\) along the path \(\lambda_{\rho}\) with the starting point \(n\) and at the depth \(d\geqslant n\), is defined inductively as follows:  
++  
**Proof of Theorem 1. ** We prove this theorem by structural induction on the formula \(\varphi\) in EMTLKD. The inductive hypothesis is that the translation preserves truth, i.e., for any subformula \(\psi\) of \(\varphi\), we have \(M\models\psi\) if and only if \(M\models\operatorname{tr}(\psi)\).