## 5 SMT-Based BMC of \(\mathsf{ELTLKD_{q}}\) Properties
### Test Formula for FTTCS in EMTLKD Logic  
In the context of the faulty timed train controller system (FTCS), we propose the following formula for testing, using the EMTLKD logic. The formula checks the system behavior under certain conditions, involving both temporal, epistemic, and deontic modalities.  
\[\mathrm{G}_{[0,\Delta)}\Big{(}\overline{\mathcal{O}}_{C}\big{(}\overline{ \mathbf{K}}_{\mathrm{T}1}\big{(}\
eg approach_{T2}\vee\mathrm{G}_{[0,\delta)} \
eg in\mathit{n}_{T2}\big{)}\wedge\overline{\mathrm{D}}_{\{T1,T2\}}out_{T1} \big{)}\Big{)}\]  
where  
* \(T1\) and \(T2\) refer to trains \(1\) and \(2\), respectively.
* \(\Delta\) is the maximum time within which either train must leave the tunnel.
* \(\delta\) is the minimum time interval that must pass before the next train can enter the tunnel.
* \(C\) represents the controller.
* \(approach_{T2}\) means that train \(T2\) is approaching the tunnel.
* \(int_{T2}\) means that train \(T2\) is inside the tunnel.
* \(out_{T1}\) means that train \(T1\) has exited the tunnel.  
This formula models the following system behavior:  
1. [label=0., ref=0]
2. Throughout the interval \([0,\Delta)\), the system checks whether the controller \(C\) is functioning correctly in at least one state, even if it may not function correctly all the time.  
2. Train \(T1\) does not have complete knowledge of whether train \(T2\) is approaching the tunnel. If \(T2\) is approaching, \(T1\) assumes that \(T2\) will not enter the tunnel for at least \(\delta\) time units, ensuring safety.
3. When train \(T1\) exits the tunnel, both trains \(T1\) and \(T2\) are aware of this fact, thanks to their distributed knowledge. This ensures proper coordination between the trains regarding tunnel usage. Specifically, it checks the following:  
1. \(G_{[0,\Delta)}\): This is the _bounded always_ operator, ensuring that everything inside the parentheses must hold continuously throughout the interval \([0,\Delta)\). The time frame \(\Delta\) represents the time during which the system's behavior is evaluated.
2. \(\overline{\mathcal{O}}_{C}\): This deontic modality asserts that the controller \(C\) is functioning correctly in at least one state during the system's operation. Unlike \(\mathcal{O}_{C}\), which would imply correct functioning in all states, \(\overline{\mathcal{O}}_{C}\) ensures that there is some state in which \(C\) operates properly, even if it is not always the case.
3. \(\overline{\mathcal{K}}_{T1}\): This epistemic modality indicates that train \(T1\) is uncertain whether or not train \(T2\) is approaching the tunnel (\(approach_{T2}\)). In this case, \(T1\) must consider the possibility that \(T2\) is approaching and be prepared for it.
4. \(-approach_{T2}\lor G_{[0,\delta)}-in_{T2}\): This part means that either train \(T2\) is not approaching the tunnel, or, if it is approaching, it is guaranteed that \(T2\) will not enter the tunnel for at least \(\delta\) time units. This ensures that even if \(T2\) approaches, there will be a delay before it enters the tunnel.
5. \(\overline{\mathcal{D}}_{\{T1,T2\}}out_{T1}\): This represents _distributed knowledge_ between trains \(T1\) and \(T2\), meaning that both trains are aware of the fact that \(T1\) has exited the tunnel (\(out_{T1}\)). This shared knowledge ensures that the system is synchronized regarding the tunnel's availability.