## 6 Conclusions  
In this paper, we investigate the verification of safety-critical systems, specifically real-time multi-agent systems (RTMASs), using SMT-based bounded model checking (BMC) for the existential fragment of deontic-epistemic metric temporal logic (EMTLKD). We introduce a novel formalism, dense-timed deontic interpreted systems (DTDISs), to model RTMASs that operate under strict timing constraints while incorporating both deontic (normative) and epistemic (knowledge-based) components. This formalism enables the analysis of both the ideal (correct) and actual (potentially faulty) behavior of agents within such systems. We propose an SMT-based approach for verifying properties expressed in EMTLKD by translating EMTLKD into a variant of deontic-epistemic linear temporal logic, \(\text{ELTLKD}_{q}\), which introduces additional propositional variables to represent dense-time semantics. The SMT-based BMC method efficiently checks for counterexamples up to a given depth, facilitating the detection of potential faults or deviations in real-time multi-agent systems. To demonstrate the practicality of our approach, we apply it to a case study involving a faulty timed train controller system. This case study illustrates how the proposed method can identify mutual exclusion violations and detect faulty behavior in systems with real-time and epistemic constraints. The results highlight the method's effectiveness in identifying critical timing and safety issues that arise due to incorrect system assumptions or violations of normative constraints. Our verification process not only determines the conditions under which safety properties hold but also reveals the circumstances leading to failures--insights that are crucial for improving system design and robustness. The contributions of this work lay the foundation for further research in the automatic verification of complex real-time multi-agent systems that require reasoning about timing, knowledge, and failures in agent behavior. Future directions include extending our approach to more intricate scenarios, integrating optimization techniques to handle larger state spaces, and applying the method to a broader range of real-world safety-critical systems. Additionally, advancing the integration of SMT solvers for more expressive temporal and epistemic logics will further enhance the applicability of the proposed verification methods in the domain of formal verification. Beyond its theoretical significance, this paper provides a practical verification framework for engineers in transportation safety and industrial automation. Future work will focus on implementing the proposed method within real-world verification workflows, thoroughly evaluating its performance and scalability. This will be essential for assessing its applicability in large-scale engineering environments and ensuring that it meets the reliability standards required in critical industries. The results of such an implementation will provide valuable insights and may lead to further improvements or refinements of the methodology. Furthermore, applying this approach to real-world transportation infrastructures, automated railway systems, or industrial automation scenarios, where distributed decision-making and real-time coordination are crucial, would provide deeper validation of its practical impact. Conceptualization: B.W.-S. and I.S. ; methodology: B.W.-S. and I.S. ; validation: B.W.-S. and I.S. ; formal analysis: B.W.-S. and I.S. ; investigation: B.W.-S., I.S. and I.O. ; writing-original draft preparation: B.W.-S., I.S. and I.O. ; writing-review and editing: B.W.-S., I.S. and I.O. ; visualization: B.W.-S.; supervision: B.W.-S.; project administration B.W.-S.; funding acquisition B.W.-S. All authors have read and agreed to the published version of the manuscript. **Informed Consent Statement:** Not applicable. **Data Availability Statement:** The original contributions presented in the study are included in the article, further inquiries can be directed to the corresponding author.