## 3 Model Checking CTL Properties
### The Standard Bottom-Up Approach  
As said previously, the QCTL properties are kind of \"state-based\" properties. The algorithm for checking whether an LQMC \(\mathfrak{M}\) satisfies a given QCTL state property \(\varphi\) mimics the similar algorithms developed for CTL and PCTL: the state formula \(\varphi\) is analyzed from bottom to top, and for each of its state subformulas, the set of states satisfying the subformula is computed. When a quantified path formula needs to be analyzed, different techniques are used according to the underlying temporal operator. Let \(\mathit{Sat}(\varphi)\) denote the set of states satisfying the QCTL state formula \(\varphi\), that is, \(\mathit{Sat}(\varphi)=\{\,s\in S\mid s\models\varphi\,\}\). The set \(\mathit{Sat}(\varphi)\) can be computed recursively on the structure of \(\varphi\) as follows. \[\mathit{Sat}(a) =\{\,s\in S\mid a\in L(s)\,\}\] \[\mathit{Sat}(\varphi_{1}\land\varphi_{2}) =\mathit{Sat}(\varphi_{1})\cap\mathit{Sat}(\varphi_{2})\] \[\mathit{Sat}(\
eg\varphi) =S\setminus\mathit{Sat}(\varphi)\] \[\mathit{Sat}(\mathbb{Q}_{\
eg\mathcal{E}}[\psi]) =\{\,s\in S\mid Q_{s}^{\mathfrak{M}}(\{\,\sigma\in\operatorname{ Path}^{\mathfrak{M}}\mid\sigma\models\psi\,\})\sim\mathcal{E}\,\}\]The above algorithm for computing the satisfaction set \(Sat(\varphi)\) of a QCTL state formula \(\varphi\) relies on the computation of the super-operator that is \(\widetilde{\sim}\)-equivalent to \(Q_{s}^{\mathfrak{M}\mathfrak{S}}\) and then \(\sim\)-compares it with \(\mathcal{E}\). The computation of \(Q_{s}^{\mathfrak{M}\mathfrak{S}}\) depends on the actual path formula that needs to be satisfied; to simplify the notation, below we just write \(Q_{s}^{\mathfrak{M}\mathfrak{S}}(\psi)\) to mean \(Q_{s}^{\mathfrak{M}\mathfrak{S}}(\{\,\sigma\in\operatorname{Path}^{ \mathfrak{M}}|\;\sigma\models\psi\,\})\). Consider the Next operator \(\mathbf{X}\). The computation of \(Q_{s}^{\mathfrak{M}\mathfrak{S}}(\mathbf{X}\varphi)\) is rather easy: by hypothesis, we already have computed \(Sat(\varphi)\), so \(Q_{s}^{\mathfrak{M}\mathfrak{S}}(\mathbf{X}\varphi)\) reduces to compute the overall super-operator leading to the successors of \(s\) that belong to \(Sat(\varphi)\), namely,  
\[Q_{s}^{\mathfrak{M}\mathfrak{S}}(\mathbf{X}\varphi)\;\widetilde{\sim}\sum_{s^ {\prime}\in\operatorname{S}\operatorname{S}\operatorname{tr}(\varphi)} \mathbf{Q}(s,s^{\prime}).\]  
Consider, now, the bounded Until operator \(\mathbf{U}^{\leq k}\). The computation of \(Q_{s}^{\mathfrak{M}\mathfrak{S}}(\varphi_{1}\,\mathbf{U}^{\leq k}\,\varphi_{2})\) is a bit more involved: since \(k\) is a given finite natural number, we can just consider \(\mathfrak{M}\mathfrak{S}\) and unfold it \(k\) times; then, we accumulate the super-operators layer by layer, as long as the states satisfy the conditions given by the semantic of \(\mathbf{U}^{\leq k}\). Formally, we have that \(Q_{s}^{\mathfrak{M}\mathfrak{S}}(\varphi_{1}\,\mathbf{U}^{\leq k}\,\varphi_{2})\) is \(\widetilde{\sim}\)-equivalent to  
\[ \begin{cases}\mathcal{I}_{\mathcal{H}}&\text{if }s\in Sat(\varphi_{2});\\ \sum_{s^{\prime}\in S}Q_{s^{\prime}}^{\mathfrak{M}\mathfrak{S}}(\varphi_{1}\, \mathbf{U}^{\leq k-1}\,\varphi_{2})\mathbf{Q}(s,s^{\prime})&\text{if }k>0\text{ and }s\in Sat( \varphi_{1})\setminus Sat(\varphi_{2});\\ 0_{\mathcal{H}}&\text{otherwise.}\end{cases} \]  
Intuitively, this is essentially the application of the Next \(\mathbf{X}\) operator \(k\) times, while checking the satisfaction of \(\varphi_{1}\) and \(\varphi_{2}\), since \(\varphi_{1}\,\mathbf{U}^{\leq k}\,\varphi_{2}\) is equivalent to \(\varphi_{2}\) when \(k=0\) and to \(\varphi_{2}\vee(\varphi_{1}\wedge\mathbf{X}(\varphi_{1}\,\mathbf{U}^{\leq k-1 }\,\varphi_{2}))\) when \(k\geq 1\). The last case, the (unbounded) Until operator \(\mathbf{U}\), is more challenging: intuitively, it is just the limit for \(k\) to infinity of the bounded case.