## 2 Dense-Timed Deontic Interpreted System
* \(\mathcal{X}_{\mathbf{c}}\) is a non-empty and finite set of _clocks_ for agent (environment) \(\mathbf{c}\). We assume that the clocks of the environment \(\mathcal{E}\) are considered \"public\". * \(P_{\mathsf{c}}:L_{\mathsf{c}}\mapsto 2^{\Sigma_{\mathsf{c}}}\) is a _local protocol_ function that maps each local state to a set of local actions that can be performed in that state. * \(\mathcal{V}_{\mathsf{c}}:L_{\mathsf{c}}\to 2^{\mathcal{P}\mathcal{V}_{ \mathsf{c}}}\) is a _valuation function_ that assigns to each local state a set of propositional variables that are true at that state. * \(\mathcal{I}_{\mathsf{c}}:L_{\mathsf{c}}\to\mathcal{C}(\mathcal{X}_{\mathsf{c}})\) is an _invariant function_ that specifies the amount of time agent (environment) \(\mathsf{c}\) may spend in its local states. * \(t_{\mathsf{c}}:L_{\mathsf{c}}\times L_{\mathcal{E}}\times\mathcal{C}( \mathcal{X}_{\mathsf{c}})\times 2^{\mathcal{X}_{\mathsf{c}}}\times\Sigma\to L_{ \mathsf{c}}\) is a (partial) _evolution function_ for agent \(\mathsf{c}\in\mathbb{A}\). This function governs the transition of agent \(\mathsf{c}\)'s local state, contingent upon the following:
* The local states of both the agent and the environment;
* The _enabling condition_ (i.e., a clock constraint from the set \(\mathcal{C}(\mathcal{X}_{\mathsf{c}})\));
* The set of clocks of the agent to be reset;
* The joint action performed. * \(t_{\mathcal{E}}:L_{\mathcal{E}}\times\mathcal{C}(\mathcal{X}_{\mathcal{E}}) \times 2^{\mathcal{X}_{\mathcal{E}}}\times\Sigma\to L_{\mathcal{E}}\) is a (partial) _evolution function_ for the environment \(\mathcal{E}\). Before we define the semantics of DTDISs, here are some additional explanations. Clocks are essential for modeling temporal aspects in a DTDIS. Each clock is represented by a continuous variable that progresses over time, with the set of clocks \(\mathcal{X}_{\mathsf{c}}\) for each agent including all clocks relevant to that agent's perspective. The evolution of clocks is governed by clock constraints \(\mathcal{C}(\mathcal{X}_{\mathsf{c}})\). Additionally, each agent, including the environment, has its own set of local states \(L_{\mathsf{c}}\) representing the possible conditions or configurations in which the agent can find itself. These states are divided into faultless (green) states \(\mathcal{G}_{\mathsf{c}}\) and faulty (red) states \(\mathcal{R}_{\mathsf{c}}\), providing a means to model system failures or abnormalities. The initial local states \(t_{\mathsf{c}}\) indicate the starting points for each agent, while evolution functions \(t_{\mathsf{c}}\) and \(t_{\mathcal{E}}\) describe how the system evolves over time. These functions specify how local states change based on the current state, environmental conditions, clock constraints, and actions taken, though they are partial because not all transitions might be defined. Each agent has a set of local actions \(\Sigma_{\mathsf{c}}\) available to it, driving the progression of the system. Joint actions, combinations of local actions taken by different agents simultaneously, are also considered. The null action \(\epsilon_{\mathsf{c}}\) represents the absence of action. Furthermore, the local protocol function \(P_{\mathsf{c}}\) determines which actions an agent can take in a given local state, while the valuation function \(\mathcal{V}_{\mathsf{c}}\) assigns truth values to propositional variables \(\mathcal{P}\mathcal{V}_{\mathsf{c}}\) based on the current local state. Finally, the invariant function \(\mathcal{I}_{\mathsf{c}}\) specifies constraints on how much time an agent can spend in its local states, ensuring adherence to predefined timing constraints. With these components in mind, we can proceed to define the semantics of a DTDIS by associating it with a _dense-timed deotic model_, which is a tuple \(M=(\Sigma,S,\iota,\to,\mathcal{V})\), where  
* \(\Sigma\) is the set of joint actions.