## 1 Introduction  
Safety-critical systems play a crucial role in multiple sectors, including transportation, healthcare, aviation, and industrial automation. A failure in these systems can have severe consequences, impacting both human lives and critical infrastructure.  
Examples of such systems are as follows:  
* Autopilot systems that ensure stable flight paths through accurate sensor data processing.
* Air traffic control systems that coordinate aircraft movements to prevent collisions using radar and real-time communication.
* Train control systems that regulate train movements and prevent crashes through automated signaling.
* Automotive safety systems such as anti-lock braking systems (ABSs), airbag deployment, and autonomous driving algorithms, which must reliably respond in real time.  
* Maritime navigation systems that use GPS and sonar to help ships navigate safely under challenging conditions.  
These systems rely on sensor networks to ensure real-time decision-making, necessitating formal verification methods to guarantee correctness under temporal and safety constraints.  
This paper focuses on the engineering challenges of ensuring compliance and correctness in such systems. Our method provides a verification framework applicable to transportation (e.g., train signaling and collision avoidance) and industrial automation (e.g., robotic control protocols). By formalizing both timing constraints and norm compliance, our approach ensures practical applicability in the verification of real-world engineering systems.  
Safety-critical systems can be represented as multi-agent systems (MASs) [1], consisting of loosely interconnected networks of _agents_ that engage in communication, coordination, negotiation, and cooperation to address challenges that exceed the skills or knowledge of any one agent. These agents are rational, autonomous entities that operate on behalf of their consumers, frequently possessing different information or conflicting interests, inside open and distributed environments.  
Furthermore, these systems can be classified as real-time systems (RTSs) [2], where correct functioning critically depends on meeting certain timing constraints. Real-time systems are infinite-state systems in which the state space contains time variables that might be discrete or continuous. The most common method for analyzing such systems is to use symbolic representation of configurations, which allows for the finite encoding of infinitely many system states.  
A real-time multi-agent system (RTMAS) combines both aspects: many interacting agents operating under real-time constraints. A practical example is a train control system, where trains must communicate and coordinate to achieve their objectives and prevent collisions. The system's correctness depends not only on effective coordination but also on strict time constraints.  
As the design of complex real-time multi-agent systems evolves, it becomes clear that agents may not always act as intended. As a result, it is critical not only to analyze properties that hold when protocols are followed correctly, but also to predict, test, and verify properties that may emerge when these protocols are violated. To address this, it is crucial to investigate scenarios where agents depart from ideal behavior and to assess how these deviations impact system results. A deontic real-time multi-agent system (DRTMAS) framework can help in this issue, as it provides a formalism to represent and reason about the distinction between ideal (correct and acceptable) behavior and actual (possibly incorrect or unacceptable) behavior.