## 2 Dense-Timed Deontic Interpreted System
### An Example of a Real-Time MAS and Its DTDIS Model
Considering the aforementioned FTCS for two trains \(T_{1}\) and \(T_{2}\), with \(\Delta=5\) and \(\delta=6\) (mutual exclusion holds under the assumption of the controller functioning correctly; otherwise, it does not), a prefix of the potential run \(\rho\) of a dense-timed deontic model for that scenario is as follows:  
include railway control, healthcare monitoring, and air traffic management. EMTLKD enables precise reasoning about agent behavior, their knowledge, and the correct functioning of components over time. The faulty timed train controller system (FTCS), as described in the previous section, offers a compelling example of how EMTLKD can be applied to the verification and analysis of multi-agent safety-critical systems. The system comprises \(n\) trains, each with individual clocks, accessing a shared tunnel controlled by a central controller \(C\). The tunnel accommodates only one train at a time; concurrent entry results in failure. This scenario is particularly interesting because while the system respects temporal constraints, a malfunctioning controller might lead to mutual exclusion violations--a critical property of the system that ensures no two trains are inside the tunnel simultaneously. EMTLKD provides a framework to express and verify the behavior of such a system by considering both temporal aspects (how long trains wait and operate) and epistemic aspects (what agents know about the state of the system). Moreover, it is particularly well suited for verifying the correctness of the system, especially in the face of unexpected failures like the faulty traffic lights remaining green. Example: Faulty Timed Train Controller System (FTCS)  
Consider a simplified version of the FTTCS with two trains, \(T_{1}\) and \(T_{2}\), and the following properties:  
* Each train \(T_{i}\) has a local clock \(x_{i}\) that tracks how long it has been waiting to enter the tunnel. * The controller \(C\) has states representing whether the tunnel is empty (state **0**), occupied by train \(T_{i}\) (state \(i\)), or in a faulty state \(F\), where it may incorrectly allow multiple trains to enter the tunnel. A critical property we want to verify is that the mutual exclusion rule is upheld: no two trains should ever be in the tunnel at the same time, unless the controller has entered the faulty state. This property can be formalized in EMTLKD as follows:  
\[\mathrm{F}(\overline{\mathrm{K}}_{C}\mathrm{F}_{[0,6)}(-t tunnel_{1}\lor-t tunnel_{2})\wedge\overline{\mathcal{O}}_{C}( \mathrm{F}_{[0,6)}(t tunnel_{1}\wedge tunnel_{2})))\]  
This specification states the following:  
* Eventually (F), it should not be the case that the controller knows (\(\overline{\mathrm{K}}_{C}\)) that both trains are in the tunnel simultaneously for any period up to 6 time units (\(\mathrm{F}_{[0,6)}\))
* It is not the case that the controller is always functioning correctly (\(\overline{\mathcal{O}}_{C}\)) to ensure that mutual exclusion holds for the same time period. This formula captures the requirement that the controller not only knows about potential safety violations but also has the responsibility to ensure that no two trains are allowed to be inside the tunnel at the same time, barring a malfunction. The strength of EMTLKD lies in its ability to model not just time-constrained actions, but also the epistemic and deontic states of agents--what they know and whether they are functioning ideally--allowing for thorough analysis and validation of these safety-critical systems.