## 2 Dense-Timed Deontic Interpreted System
### An Example of a Real-Time MAS and Its DTDIS Model  
To illustrate the application of dense-timed deontic interpreted systems (DTDISs), consider a faulty version of the _timed train controller system_ (FTCS) [38], also known as Fischer's mutual exclusion protocol. Unlike the original system, where correctness is inherently tied to the time constraints, the flawed version does not violate these temporal conditions but introduces unexpected erroneous behavior from the controller. This scenario closely mirrors real-world failures in automated railway control systems, where misconfigurations or faulty controllers have caused severe accidents, such as train collisions due to incorrect signal interpretations. By applying formal verification techniques like our DTDIS model, engineers can detect such flaws early, ensuring safer and more reliable railway systems. The FTTCS consists of the following:  
* \(n\) trains (\(T_{1},\ldots,T_{n}\), where \(n\geq 2\)), each traversing its dedicated circular track unidirectionally and equipped with an individual clock \(y_{i}\). * A controller \(C\) responsible for managing train access to a tunnel, a crucial section of the track used by all trains. * An environment \(\mathcal{E}\) that encompasses external factors affecting the system. Since the tunnel accommodates only one track, trains traveling in opposite directions cannot use it simultaneously. To regulate this, traffic lights at both ends of the tunnel alternate between red and green. Trains communicate their entry and exit from the tunnel to the controller. However, in the faulty version, the controller may fail--allowing traffic lights to remain green despite a train's entry, leading to potential collisions. This system scales according to the number of trains (\(n\)), with each train functioning as an independent agent. Figure 1 illustrates the local states, possible local actions, local clocks, clock constraints, invariants, and the local protocol for each agent, excluding the environment \(\mathcal{E}\). Null actions are not depicted in Figure 1. Additionally, the states colored green belong to the faultless (green) set of the respective agent, while those colored red belong to the faulty (red) set. When in the state \(away\), train \(T_{i}\) can signal its intent to enter the tunnel, provided that the value of the controller \(C\) is zero (indicating that no other train has made the same request). Subsequently, it transitions to the state \(try\), where it waits for an arbitrary duration, less than \(\Delta\) time units, before updating \(C\) to \(i\). At this point, it becomes poised to enter the tunnel; however, a minimum time interval of \(\delta\) is required for this transition. Upon exiting the tunnel, the train sets \(C\) to the state \(0\). Figure 1: A faulty timed train controller system. Controller \(C\) has \(n+2\) states, indicating that all trains are _away_ (state 0), the numbers of trains, i.e., \(1,\ldots,n\), and that the controller is faulty (i.e., faulty traffic lights remain green when a train enters the tunnel). Controller \(C\) is initially at state 0. It moves to state \(i\) if it is notified by train \(T_{i}\). While in state \(i\), it can either return to state 0, or \"jump\" to state \(j\) when notified by train \(T_{j}\). Furthermore, the controller has the capability to transition from states 1 through \(n\) to state \(F\) due to damage or malfunction. It may persist in this state and, upon restoration, return to state 0. Moreover, while in state \(F\), the controller permits the entry of a waiting train outside the tunnel, even if another train is currently inside. The action \(start_{i}\) of train \(T_{i}\) signifies the transition from the _away_ state to the state where the train seeks access to the tunnel. As previously mentioned, this transition is permissible only if controller \(C\) is in state 0. This restriction is maintained by the synchronization of train \(T_{i}\) with controller \(C\) upon the action \(start_{i}\), which is enabled exclusively when \(C\) is in state 0.