## 2 Dense-Timed Deontic Interpreted System
* \(S=\prod_{\mathsf{c}\in\mathsf{A}\cup\{\mathcal{E}\}}(L_{\mathsf{c}}\times \mathbb{R}^{|\mathcal{X}_{\mathsf{c}}|})\) is the non-empty set of all _global states_ such that \(L_{\mathsf{c}}\supseteq\mathcal{G}_{\mathsf{c}}\). For a global state \(s=((\ell_{1},v_{1}),\ldots,(\ell_{n},v_{n}),(\ell_{\mathcal{E}},v_{\mathcal{ E}}))\in S\), the symbol \(l_{\mathsf{c}}(s)=\ell_{\mathsf{c}}\) denotes the local component of agent \(\mathsf{c}\in\mathsf{A}\cup\{\mathcal{E}\}\) in \(s\), and \(v_{\mathsf{c}}(s)=v_{\mathsf{c}}\) denotes the clock valuation of agent \(\mathsf{c}\in\mathsf{A}\cup\{\mathcal{E}\}\) in \(s\). * \(\iota=\prod_{\mathsf{c}\in\mathsf{A}\cup\{\mathcal{E}\}}(\iota_{\mathsf{c}} \times\{0\}^{|\mathcal{X}_{\mathsf{c}}|})\) is the non-empty set of all _initial global states_ such that \(\iota\subseteq S\). * \(\to\subseteq S\times(\Sigma\cup\mathbb{R})\times S\) is a transition relation defined by action and time transitions:
* Action transition: for any \(\overline{\imath}\in\Sigma\), \(s\stackrel{{\overline{\imath}}}{{\longrightarrow}}s^{\prime}\) iff for all \(\mathsf{c}\in\mathbb{A}\), there exists a transition \(t_{\mathsf{c}}(l_{\mathsf{c}}(s),l_{\mathsf{c}}(s),\epsilon_{\mathsf{c}\mathsf{ c}},Y,\overline{\pi})=l_{\mathsf{c}}(s^{\prime})\) such that \(v_{\mathsf{c}}(s)\models\epsilon_{\mathsf{c}}\wedge\mathcal{I}_{\mathsf{c}}(l_{ \mathsf{c}}(s))\) and \(v_{\mathsf{c}}^{\prime}(s^{\prime})=v_{\mathsf{c}}(s)[Y:=0]\) and \(v_{\mathsf{c}}^{\prime}(s^{\prime})\models\mathcal{I}_{\mathsf{c}}(l_{ \mathsf{c}}(s^{\prime}))\), and there exists a transition \(t_{\mathcal{E}}(l_{\mathcal{E}}(s),\epsilon_{\mathcal{E}},Y,\overline{\pi})=l_{ \mathcal{E}}(s^{\prime})\) such that \(v_{\mathcal{E}}(s)\models\epsilon_{\mathcal{E}}\wedge\mathcal{I}_{\mathcal{E}} (l_{\mathcal{E}}(s))\) and \(v_{\mathcal{E}}^{\prime}(s^{\prime})=v_{\mathcal{E}}(s)[X^{\prime}:=0]\) and \(v_{\mathcal{E}}^{\prime}(s^{\prime})\models\mathcal{I}_{\mathcal{E}}(l_{ \mathcal{E}}(s^{\prime}))\). Time transition: let \(\delta\in\mathbf{R}_{+}\), \(s\stackrel{{\delta}}{{\longrightarrow}}s^{\prime}\) iff for all \(\mathbf{c}\in\mathbb{A}\cup\{\mathcal{E}\}\), \(l_{\mathbf{c}}(s)=l_{\mathbf{c}}(s^{\prime})\) and \(v_{\mathbf{c}}(s)\models\mathcal{I}_{\mathbf{c}}(l_{\mathbf{c}}(s))\) and \(v_{\mathbf{c}}^{\prime}(s^{\prime})=v_{\mathbf{c}}(s)+\delta\) and \(v_{\mathbf{c}}^{\prime}(s^{\prime})\models\mathcal{I}_{\mathbf{c}}(l_{ \mathbf{c}}(s))\). * \(\mathcal{V}:S\to 2^{\mathcal{P}V}\) is the valuation function defined as \(\mathcal{V}(s)=\bigcup_{\mathbf{c}\in\mathbb{A}\cup\{\mathcal{E}\}}\mathcal{V }_{\mathbf{c}}(l_{\mathbf{c}}(s))\). We assume that the relation \(\to\) is total, meaning that for any \(s\in S\), there exists \(s^{\prime}\in S\), along with either a non-empty joint action \(\overline{a}\in\Sigma\) or a real number \(\delta\in\mathbf{R}\), such that \(s\stackrel{{\overline{a}}}{{\longrightarrow}}s^{\prime}\) or \(s\stackrel{{\delta}}{{\longrightarrow}}s^{\prime}\) holds. This ensures the possibility of transitioning from any state to another through either action execution or time passage. Furthermore, for a given DTDIS and an agent \(\mathbf{c}\in\mathbb{A}\), we define the following:  
* _Indistinguishability relation_: For any \(s,s^{\prime}\in S\), we denote \(s\sim_{\mathbf{c}}s^{\prime}\) if and only if \(l_{\mathbf{c}}(s^{\prime})=l_{\mathbf{c}}(s)\). This relation captures states that are indistinguishable from the perspective of the agent \(\mathbf{c}\). * _Deontic relation_: For any \(s\in S\), we denote \(s\propto_{\mathbf{c}}s^{\prime}\) if and only if \(l_{\mathbf{c}}(s^{\prime})\in\mathcal{G}_{\mathbf{c}}\). This relation signifies states that are permissible or compliant with the agent's objectives or requirements.