## 3 Model Checking CTL Properties
### The Standard Bottom-Up Approach
However, a naive computation of such a limit is likely to be inefficient, so it is preferable to adopt a different approach, such as the one underlying the PCTL model checking algorithm that is based on a fixed point computation. To this end, we partition the state space \(S\) into three sets: \(S^{\mathcal{I}_{\mathcal{H}}}\), with all states that we are sure satisfy \(\varphi_{1}\,\mathbf{U}\,\varphi_{2}\); we can assign the super-operator \(\mathcal{I}_{\mathcal{H}}\) to these states. \(S^{0_{\mathcal{H}}}\), containing the states that we are sure do not satisfy \(\varphi_{1}\,\mathbf{U}\,\varphi_{2}\); we can assign the super-operator \(0_{\mathcal{H}}\) to these states. \(S^{7}\), for the remaining states for which we do not know whether they satisfy \(\varphi_{1}\,\mathbf{U}\,\varphi_{2}\) and for which we cannot assign a predefined super-operator. States that belong to \(S^{\mathcal{I}_{\mathcal{H}}}\) are clearly those in \(Sat(\varphi_{2})\), as well as those in \(Sat(\varphi_{1})\) that cannot avoid to reach \(S^{\mathcal{I}_{\mathcal{H}}}\) in one step. Symmetrically, it is certain that the states in \(S\setminus(Sat(\varphi_{1})\cup Sat(\varphi_{2}))\) belong to \(S^{0_{\mathcal{H}}}\), since they clearly violate \(\varphi_{1}\,\mathbf{U}\,\varphi_{2}\); moreover, also the states that have no way to reach \(Sat(\varphi_{2})\) in the underlying graph can be included in \(S^{0_{\mathcal{H}}}\). Regarding the super-operator to assign at the states in \(S^{7}\), by [44] (Theorem 5.1) it is the least fixed point of the function \(f(X)=X\mathcal{T}+\mathcal{G}\), where \(\mathcal{T}\) and \(\mathcal{G}\) are two matrices indexed by the states in \(S^{7}\) and whose entries depend on \(\mathbf{Q}\). More formally, Theorem 5.1 of [44] shows that, given the matrices \(\mathcal{T}=(\mathbf{Q}(s^{\prime},s))_{s^{\prime}\in S^{7}}\) of size \(|S^{7}|\times|S^{7}|\) and \(\mathcal{G}=(\sum_{s^{\prime}\in S^{7_{\mathcal{H}}}}\mathbf{Q}(s,s^{\prime} ))_{s\in S^{7}}\) of size \(1\times|S^{7}|\), it holds that \(Q_{s}^{\mathfrak{M}\mathfrak{S}}(\varphi_{1}\,\mathbf{U}\,\varphi_{2})\)\(\widetilde{\mathcal{E}}_{s}\), where \(\widetilde{\mathcal{E}}\) is the least fixed point of \(f(X)=X\mathcal{T}+\mathcal{G}\) and \(\widetilde{\mathcal{E}}_{s}\) is the entry of \(\widetilde{\mathcal{E}}\) relative to the state \(s\). The matrix \(\mathcal{G}\) represents the super-operators that lead each state \(s\in S^{7}\) to the goal set \(S^{\mathcal{I}_{\mathcal{H}}}\) in one step; the matrix \(\mathcal{T}\) instead contains the super-operators that in one step lead each state \(s\in S^{7}\) to other states also in \(S^{7}\). Note that we do not need to consider the super-operators leading to \(S^{0_{\mathcal{H}}}\) since they would lead to a failure in satisfying the formula \(\varphi_{1}\,\mathbf{U}\,\varphi_{2}\). Detailed algorithms for the computation of \(Q_{s}^{\mathfrak{M}\mathfrak{S}}(\varphi_{1}\,\mathbf{U}\,\varphi_{2})\), based on Jordan decomposition or matrix inversion, can be found in [49, 50]. **Example 1**. : _As an example of application of quantum CTL, consider the QMC shown in Figure 1 and its labelled counterpart where each classical state \(\ell_{i}\) obtains label \(\ell_{i}\), that is, we only assign the state name as the label for the state. As formula, consider \(Q_{\widetilde{\times}\mathcal{I}_{\mathcal{H}}}[(-\ell_{2})\,\mathbf{U}\,\ell_{ 3}]\), which requires to check whether the super-operator corresponding to the paths that eventually reach \(\ell_{3}\) without passing through \(\ell_{2}\) is at least \(\mathcal{I}_{\mathcal{H}}\). The algorithm for model checking this property works as follows: we start from the state properties in the leaves of the parsing tree of \(\mathbb{Q}_{\gtrsim\mathcal{I}_{\mathcal{H}}}[(-\ell_{2})\ \mathbf{U}\,\ell_{3}]\), that is, \(\ell_{2}\) and \(\ell_{3}\), and we compute \(\operatorname{\text{Sat}}(\ell_{2})=\{\ell_{2}\}\) and \(\operatorname{\text{Sat}}(\ell_{3})=\{\ell_{3}\}\). Then, we compute \(\operatorname{\text{Sat}}(-\ell_{2})=\{\ell_{0},\ell_{1},\ell_{3}\}\).