## 1 Introduction
### Automatic Verification  
Ensuring the correctness of multi-agent and real-time systems is challenging due to the complexity of their interactions and timing constraints. A key difficulty is the state explosion problem, which arises as the number of system components increases exponentially. To address this issue, various automatic verification techniques have been developed. Among these, model checking [15] has emerged as the most prominent method for systematically verifying whether a system satisfies a given specification. In model checking, a system is encoded as a transition system, and its specification is represented as a logical formula. If the property does not hold, a counterexample demonstrating the cause of the problem is identified [16]. Model checking techniques can be broadly categorized as follows:  
* Symbolic approaches (BDD-based methods) --these methods use compact representations of state spaces to efficiently handle large verification problems. However, they often suffer from scalability limitations. * SAT-based Bounded Model Checking (BMC)--efficient for finite-state systems but not well suited for dense-time properties. * SMT-based Bounded Model Checking (BMC)--extends SAT-based BMC by incorporating richer logical theories, making it more suitable for verifying real-time and epistemic properties. One of the earliest advancements in model checking was symbolic model checking, which introduced symbolic storage methods based on Binary Decision Diagrams (BDDs) [17; 18; 19]. BDD-based techniques enable efficient representation of state spaces but become infeasible for large-scale systems due to exponential memory requirements. To address these limitations, bounded model checking (BMC) was introduced as a complementary technique. Bounded model checking (BMC) [20] is a verification method primarily designed to locate counterexamples by unrolling the system's behavior up to a fixed depth. Given a model \(M\), a property \(P\), and a bound \(k\) (a natural number), BMC generates a formula \(F\) that is satisfiable if and only if there exists a counterexample of depth less than or equal to \(k\). SAT-based BMC encodes \(F\) as a propositional formula, which is then checked by a SAT solver. It was initially proposed for linear-time temporal logic (LTL) [20] and later extended to handle various other logics, including the existential fragments of CTL [21], CTLK [22], and LTLK [23] for epistemic properties, TCTLK [24] and RTCTLK [25; 26] for real-time and knowledge-based verification, and MTLKD [27] and ECTL\({}^{*}\)KD [5] for deontic and epistemic reasoning. While SAT-based BMC is effective for finite-state systems, it struggles with dense-time constraints, which are crucial in real-time multi-agent systems. The Satisfiability Modulo Theories (SMT) problem [28] extends SAT by incorporating predicates from richer mathematical theories, such as linear real arithmetic and integer arithmetic. SMT-based BMC translates the verification problem into a quantifier-free formula in a decidable subset of first-order logic, which is then checked by an SMT solver. SMT-based BMC has been successfully applied in embedded software analysis and verification written in ANSI-C [29], timed automata verification for properties expressible in TCTL [30], weighted timed automata for finding quasi-optimal runs [31], and multi-agent system verification, where different variants of interpreted systems have been analyzed [32; 33; 34]. Recent advances in SMT-based BMC [32] have demonstrated its feasibility for verifying real-time and epistemic systems. However, existing SMT-based techniques focus primarily on classical temporal or epistemic properties and do not integrate deontic reasoning, which is essential for modeling compliance and norm violations in multi-agent systems. Our approach extends SMT-based BMC by incorporating deontic constraints into the verification process, enabling a more comprehensive analysis of agent behavior in safety-critical systems.