## 5 SMT-Based BMC of \(\mathsf{ELTLKD_{q}}\) Properties
### Translation to SMT  
In this section, we describe how to encode the BMC problem for \(\operatorname{ELTLKD}_{\mathrm{q}}\) properties in a dense-timed deontic model using SMT. This translation is based on the approach outlined in [7] and involves the conversion of both the transition relations in the dense-timed deontic model \(M\) and the \(\operatorname{ELTLKD}_{\mathrm{q}}\) formula \(\operatorname{tr}(\varphi)\) into quantifier-free first-order formulas. Let \(M\) be a dense-timed deontic model, \(\varphi\) an EMTLKD formula, \(\psi=\operatorname{tr}(\varphi)\) the corresponding \(\operatorname{ELTLKD}_{\mathrm{q}}\) formula, and \(k\in\mathbb{N}\) a bound. The SMT-based bounded model checking (BMC) method translates the BMC problem \(M\models_{k}\psi\) into the satisfiability problem of the following formula:  
\[[M,\psi]_{k}:=[M^{\psi,\iota}]_{k}\wedge[\psi]_{M,k}\]  
The formula \([M,\psi]_{k}\) assumes that every global state \(s\in S\) in \(M\) can be represented by a symbolic global state \(\overline{\mathbf{w}}=(\overline{\mathbf{w}}_{1},\ldots,\overline{\mathbf{w} }_{n},\overline{\mathbf{w}}_{\mathcal{E}})\), which consists of symbolic local states for each agent. Each symbolic local state \(\overline{\mathbf{w}}_{\mathbf{c}}\) is represented as a pair:  
\[\overline{\mathbf{w}}_{\mathbf{c}}=(w_{\mathbf{c}},\mathbf{v}_{\mathbf{c}})\]  
Here, \(w_{\mathbf{c}}\) is an integer representing the local state of agent \(\mathbf{c}\), and \(\mathbf{v}_{\mathbf{c}}\) is a real variable representing the clock valuation of that agent. Similarly, each action \(a\in\Sigma\) is represented by a symbolic joint action \(\overline{\mathbf{a}}\), which is a vector of variables ranging over natural numbers. The formula \([M^{\psi,\iota}]_{k}\) imposes constraints on the symbolic \(k\)-paths to ensure they remain valid within the model \(M\). These paths must respect the transition relation of the model, both in terms of action transitions and time transitions. Conversely, the formula \([\psi]_{M,k}\) encapsulates the constraints that must be satisfied by these \(k\)-paths for \(\psi=\operatorname{tr}(\varphi)\) to hold true. The number of symbolic \(k\)-paths required to validate \(\psi\) depends on the formula and is given by the function \(f_{k}:\operatorname{EMTLKD}\to\mathbb{N}\), which we define as follows:  
\[f_{k}(\mathbf{t})=f_{k}(\mathbf{f})=f_{k}(p)=f_{k}(\
eg p)=0,\quad\text{where} \quad p\in\mathcal{PV}^{\prime},\]  
\[f_{k}(\alpha\wedge\beta)=f_{k}(\alpha)+f_{k}(\beta),\]  
\[f_{k}(\alpha\cup\beta)=k\cdot f_{k}(\alpha)+f_{k}(\beta)+1,\]  
\[f_{k}(\alpha\cup\beta)=(k+1)\cdot f_{k}(\alpha)+1,\]  
\[f_{k}(\overline{\mathbf{C}}_{\Gamma}\alpha)=f_{k}(\alpha)+k,\]  
\[f_{k}(Y\alpha)=f_{k}(\alpha)+1\quad\text{for}\quad Y\in\{\overline{\mathbf{K }}_{\mathbf{c}},\overline{\mathbf{D}}_{\Gamma},\overline{\mathbf{E}}_{\Gamma},\overline{\mathbf{O}}_{\mathbf{c}},\mathbf{K}_{\mathbf{c}_{1}}^{2}\}.\]Since in the BMC method we deal with existential validity, the number of \(k\)-paths sufficient to validate \(\psi\) is given by the function \(\widehat{f}_{k}:\mathrm{EMTLKD}\to\mathbf{N}\), which is defined as follows:  
\[\widehat{f}_{k}(\psi)=f_{k}(\psi)+1.\]  
We adopt several auxiliary quantifier-free first-order formulas, following the definitions in [42]. These formulas capture various aspects of the model \(M\):  
* \(I_{s}(\overline{\mathbf{w}})\): Encodes the fact that the state \(s\) is an initial state of the model \(M\). * \(p(\overline{\mathbf{w}})\): Encodes the propositional variable \(p\in\mathcal{PV}\) that holds in the global state \(\overline{\mathbf{w}}\). * \(H_{\mathbf{c}}(\overline{\mathbf{w}}_{\mathbf{c}},\overline{\mathbf{w}}_{ \mathbf{c}}^{\prime})\): Encodes the equivalence between two local states of agent \(\mathbf{c}\). * \(HO_{\mathbf{c}}(\overline{\mathbf{w}}_{\mathbf{c}})\): Encodes that the local state of agent \(\mathbf{c}\) is \"green\", relevant in deontic logic.