## 4 Translation from EMTLKD to \(\mathrm{ELTLKD_{q}}\)
For atomic propositions \(p\in\mathcal{PV}\):  
\[\operatorname{tr}(p)=p\quad\text{and}\quad\operatorname{tr}(\
eg p)=\
eg p.\]  
In both EMTLKD and \(\operatorname{ELTLKD}_{q}\), atomic propositions and their negations are interpreted identically, so  
\[M\models p\text{ \emph{iff} }M\models\operatorname{tr}(p)\text{ and }M\models\
eg p\text{ \emph{iff} }M\models\operatorname{tr}(\
eg p).\]  
Thus, the translation preserves truth for atomic propositions and their negations. _Inductive Step: Boolean Connectives_  
Let \(\varphi=\alpha\wedge\beta\). By the translation rules, \(\operatorname{tr}(\alpha\wedge\beta)=\operatorname{tr}(\alpha)\wedge \operatorname{tr}(\beta)\). By the inductive hypothesis, we know that \(M\models\alpha\)_iff_\(M\models\operatorname{tr}(\alpha)\) and \(M\models\beta\)_iff_\(M\models\operatorname{tr}(\beta)\). Thus,  
\[M\models\alpha\wedge\beta\text{ \emph{iff} }M\models\operatorname{tr}(\alpha)\wedge \operatorname{tr}(\beta),\]  
which implies that \(M\models\varphi\)_iff_\(M\models\operatorname{tr}(\varphi)\). The proof for \(\vee\) follows similarly. _Inductive Step: Temporal Operators_  
Let \(\varphi=\alpha\operatorname{U}_{I}\beta\). By the translation rules, \(\operatorname{tr}(\alpha\operatorname{U}_{I}\beta)=\operatorname{tr}(\alpha) \operatorname{U}(\operatorname{tr}(q_{I})\wedge\operatorname{tr}(\beta))\), where \(q_{I}\) is a condition representing that the interval \(I\) holds. By the semantics of \(\operatorname{U}_{I}\) in EMTLKD, \(\alpha\operatorname{U}_{I}\beta\) means that \(\beta\) must hold at some point within interval \(I\), and \(\alpha\) must be true at all preceding points. In \(\operatorname{ELTLKD}_{q}\), the translation ensures that \(\beta\) holds in the interval \(I\), as encoded by the condition \(\operatorname{tr}(q_{I})\wedge\operatorname{tr}(\beta)\), and that \(\alpha\) holds at preceding points. By the inductive hypothesis, \(M\models\alpha\text{ \emph{iff} }M\models\operatorname{tr}(\alpha)\) and \(M\models\beta\text{ \emph{iff} }M\models\operatorname{tr}(\beta)\). Therefore,  
\[M\models\alpha\operatorname{U}_{I}\beta\text{ \emph{iff} }M\models\operatorname{tr}(\alpha) \operatorname{U}(\operatorname{tr}(q_{I})\wedge\operatorname{tr}(\beta)),\]  
which implies that  
\[M\models\varphi\text{ \emph{iff} }M\models\operatorname{tr}(\varphi).\]  
Let \(\varphi=\operatorname{G}_{I}\beta\). By the translation rules, \(\operatorname{tr}(\operatorname{G}_{I}\beta)=\operatorname{G}(\
eg\operatorname {tr}(q_{I})\vee\operatorname{tr}(\beta))\), where \(\
eg q_{I}\) ensures that the interval \(I\) does not end prematurely. By the semantics of \(\operatorname{G}_{I}\), \(\beta\) must hold continuously throughout the interval \(I\). The translation ensures this by encoding the condition \(\
eg\operatorname{tr}(q_{I})\vee\operatorname{tr}(\beta)\), which guarantees that \(\beta\) holds as long as \(I\) holds. By the inductive hypothesis, \(M\models\beta\text{ \emph{iff} }M\models\operatorname{tr}(\beta)\), so  
\[M\models\operatorname{G}_{I}\beta\text{ \emph{iff} }M\models\operatorname{G}(\
eg \operatorname{tr}(q_{I})\vee\operatorname{tr}(\beta)),\]  
which implies that \(M\models\varphi\text{ \emph{iff} }M\models\operatorname{tr}(\varphi)\). _Inductive Step: Epistemic and Deontic Operators_  
For any epistemic operator \(\operatorname{\overline{K}}_{\mathsf{c}},\operatorname{\overline{D}}_{ \mathsf{T}},\operatorname{\overline{C}}_{\mathsf{T}},\operatorname{\overline {E}}_{\mathsf{T}},\operatorname{\overline{K}}_{\mathsf{c}}^{\mathsf{c}}\) and deontic operator \(\operatorname{\overline{O}}_{\mathsf{c}}\), the translation function preserves the structure directly, i.e., \(\operatorname{tr}(\gamma\alpha)=\gamma\operatorname{tr}(\alpha)\). By the inductive hypothesis, \(M\models\alpha\text{ \emph{iff} }M\models\operatorname{tr}(\alpha)\).