From Quantified CTL to QBF

TL;DR

This paper introduces a model-checking algorithm for QCTL, an extension of CTL with propositional quantification, by reducing the problem to QBF and comparing different strategies using Z3.

Contribution

It presents a novel reduction-based model-checking algorithm for QCTL, leveraging QBF solving techniques and evaluating various reduction strategies.

Findings

Reduction strategies vary in efficiency

Prototype implementation with Z3 demonstrates feasibility

QCTL model checking is PSPACE-complete in structure semantics

Abstract

QCTL extends the temporal logic CTL with quantifications over atomic propositions. This extension is known to be very expressive: QCTL allows us to express complex properties over Kripke structures (it is as expressive as MSO). Several semantics exist for the quantifications: here, we work with the structure semantics, where the extra propositions label the Kripke structure (and not its execution tree), and the model-checking problem is known to be PSPACE-complete in this framework. We propose a model-checking algorithm for QCTL based on a reduction to QBF. We consider several reduction strategies, and we compare them with a prototype (based on the SMT-solver Z3) on several examples.

Tables

Table 1. Table 1 : Reduction for basic modalities for reductions  UU  and   FP

	${\widehat{\neg \phi }}^{x,P}$	$=\neg {\hat{\phi }}^{x,P}{\widehat{\phi \vee \psi }}^{x,P}={\hat{\phi }}^{x,P}\vee {\hat{\psi }}^{x,P}{\widehat{\text{E}\text{X}\phi }}^{x,P}=\underset{(x,x^{\prime })\in E}{\bigvee }{\hat{\phi }}^{x^{\prime },P}$
	${\widehat{\exists p.\phi }}^{x,P}$

Table 2. Table 2 : Reduction for temporal modalities E U and A U – variant UU

	${\widehat{\text{E}\phi \text{U}\psi }}^{x,P}$	$={\overline{\text{E}\phi \text{U}\psi }}^{x,P,\left\{x\right\}}\text{with:}$		(4)
	${\overline{\text{E}\phi \text{U}\psi }}^{x,P,X}$	$={\hat{\psi }}^{x,P}\vee \left({\hat{\phi }}^{x,P}\wedge \underset{(x,x^{\prime })\in Es.t.x^{\prime }\notin X}{\bigvee }{\overline{\text{E}\phi \text{U}\psi }}^{x^{\prime },P,X\cup \left\{x^{\prime }\right\}}\right)$		(5)
	${\widehat{\text{A}\phi \text{U}\psi }}^{x,P}$	$={\overline{\text{A}\phi \text{U}\psi }}^{x,P,\left\{x\right\}}\text{with:}$		(6)
	${\overline{\text{A}\phi \text{U}\psi }}^{x,P,X}$			(7)

Table 3. Table 3 : Transformation rules for method  FBV

	${\widehat{\phi \wedge \psi }}^{x,P}$	$={\hat{\phi }}^{x,P}\wedge {\hat{\psi }}^{x,P}{\widehat{\phi \vee \psi }}^{x,P}={\hat{\phi }}^{x,P}\vee {\hat{\psi }}^{x,P}{\widehat{\neg p}}^{x,P}=\neg {\hat{p}}^{x,P}$
	${\widehat{\text{E}\text{X}\phi }}^{x,P}$	$=\underset{(x,y)\in E}{\bigvee }{\hat{\phi }}^{y,P}{\widehat{\text{A}\text{X}\phi }}^{x,P}=\underset{(x,y)\in E}{\bigwedge }{\hat{\phi }}^{y,P}{\widehat{\text{A}\text{G}\phi }}^{x,P}=\underset{(x,y)\in E^{\ast }}{\bigwedge }{\hat{\phi }}^{y,P}$
	$\text{For}Q\in \{\exists ,\forall \}$	${\widehat{Qp.\phi }}^{x,P}=Q{p}^{v_1}\dots p^{v_n}{\hat{\phi }}^{x,P\cup \left\{p\right\}}$
	$\text{For}Q\in \{\exists ,\forall \}$
	${\hat{p}}^{x,P}=$

Equations

$$\mathsf{QCTL}\ni \phi ,\psi$$

$$\mathcal{K},x\models$$

$$\text{ for any }0\le j<i,\text{ we have }\mathcal{K},\rho (j)\models \phi$$

$$\mathcal{K},x\models$$

$$\text{ for any }0\le j<i,\text{ we have }\mathcal{K},\rho (j)\models \phi$$

$$\mathcal{K},x\models$$

$${\text{E}}_{=1}\text{F}(\phi )$$

$${\text{E}}_{=1}\text{X}\phi$$

$${\text{E}}_{\ge k}\text{X}\phi =$$

$$\exists^{1}p.\varphi=\exists p.\big{(}(\text{{E}}_{=1}\text{{F}}\>p)\wedge\varphi\big{)}\quad\quad\quad\forall^{1}p.\varphi=\forall p.\big{(}(\text{{E}}_{=1}\text{{F}}\>p)\Rightarrow\varphi\big{)}$$

$$\mathcal{K},x{\models }_{\epsilon }p$$

$$\mathcal{K},x{\models }_{\epsilon }\exists p.\phi$$

$$\mathsf{QBF}\ni \alpha ,\beta \text{vbox}:\text{vbox}:=q\mid \alpha \wedge \beta \mid \alpha \vee \beta \mid \neg \alpha \mid \alpha \iff \beta \mid \alpha \Rightarrow \beta \mid \exists q.\alpha \mid \forall q.\alpha$$

$$\text{{E}}\varphi\text{{U}}\psi\quad\equiv\quad\forall z.\Big{(}\text{{A}}\text{{G}}\big{(}z\Leftrightarrow(\psi\vee(\varphi\wedge\text{{E}}\text{{X}}\>z))\big{)}\;\Rightarrow\;z\Big{)}$$

$$\text{{A}}\varphi\text{{U}}\psi\quad\equiv\quad\forall z.\Big{(}\text{{A}}\text{{G}}\big{(}z\Leftrightarrow(\psi\vee(\varphi\wedge\text{{A}}\text{{X}}\>z))\big{)}\;\Rightarrow\;z\Big{)}$$

$${\widehat{\text{A}\text{G}\phi }}^{x,P}$$

$$\mathcal{K},x{\models }_{\epsilon }\phi \text{mbox}iff{v}_{\epsilon }\models {\widehat{\mathsf{fpc}(\phi )}}^{x,\mathsf{dom}(\epsilon )}$$

$$\exists\{\kappa_{1}\ldots\kappa_{m}\}.\Big{(}\Phi_{0}\wedge\bigwedge_{i=1\ldots m}\text{{A}}\text{{G}}(\kappa_{i}\Leftrightarrow\theta_{i})\Big{)}$$

$$\Phi$$

$$\displaystyle\stackrel{{\scriptstyle i.h.}}{{\equiv}}\exists\kappa_{m}.\Big{[}\Big{(}\exists\{\kappa_{1}\ldots\kappa_{m-1}\}.\Big{(}\Phi_{0}\wedge\bigwedge_{i=1\ldots m-1}\text{{A}}\text{{G}}(\kappa_{i}\Leftrightarrow\theta_{i})\Big{)}\Big{)}\wedge\text{{A}}\text{{G}}(\kappa_{m}\Leftrightarrow\varphi_{m})\Big{]}$$

$$\displaystyle\equiv\exists\{\kappa_{1}\ldots\kappa_{m}\}.\Big{(}\Phi_{0}\wedge\bigwedge_{i=1\ldots m}\text{{A}}\text{{G}}(\kappa_{i}\Leftrightarrow\theta_{i})\Big{)}$$

$$\exists z.\forall p.\forall z^{\prime}.\Big{(}(\text{{E}}\text{{X}}(z\wedge z^{\prime})\Rightarrow\text{{A}}\text{{X}}(z\Rightarrow z^{\prime}))\wedge\text{{E}}\text{{X}}(z\wedge(\text{{A}}\text{{X}}p\vee\text{{A}}\text{{X}}\neg p))\Big{)}$$

$$\forall i,\mathcal{K},x{\models }_{\epsilon \circ {\epsilon }^{\prime }}{\theta }_i\Rightarrow \mathcal{K},x{\models }_{{\epsilon }^{\prime }}{\phi }_i\text{mbox}and\mathcal{K},x{\models }_{\epsilon \circ {\epsilon }^{\prime }}{\Phi }_0\Rightarrow \mathcal{K},x{\models }_{{\epsilon }^{\prime }}\widetilde{{\Phi }_0}$$

$$\displaystyle\stackon[-8pt]{$\text{{A}}\text{{G}}(\kappa_{i}\Rightarrow\text{{E}}\varphi\text{{W}}\psi)$}{\vstretch{1.5}{\hstretch{15}{\widehat{\phantom{\;}}}}}^{\;\;x,P}=$$

$$\displaystyle\stackon[-8pt]{$\text{{A}}\text{{G}}(\kappa_{i}\Rightarrow\text{{A}}\varphi\text{{W}}\psi)$}{\vstretch{1.5}{\hstretch{15}{\widehat{\phantom{\;}}}}}^{\;\;x,P}=$$

$$\displaystyle\stackon[-8pt]{$\text{{A}}\text{{G}}(\overline{\kappa_{i}}\Rightarrow\text{{E}}\varphi\text{{U}}\psi)$}{\vstretch{1.5}{\hstretch{15}{\widehat{\phantom{\;}}}}}^{\;\;x,P}=$$

$$\displaystyle\wedge\bigwedge_{1\leq d<|V|}\Big{(}[\overline{\kappa_{i}}^{y}=d]\Rightarrow\big{(}\widehat{\varphi}^{y,P}\wedge\bigvee_{(y,y^{\prime})\in E}[\overline{\kappa_{i}}^{y^{\prime}}=d-1]\big{)}\Big{)}\Big{]}$$

$$\displaystyle\stackon[-8pt]{$\text{{A}}\text{{G}}(\overline{\kappa_{i}}\Rightarrow\text{{A}}\varphi\text{{U}}\psi)$}{\vstretch{1.5}{\hstretch{15}{\widehat{\phantom{\;}}}}}^{\;\;x,P}=$$

$$\displaystyle\wedge\bigwedge_{1\leq d<|V|}\Big{(}[\overline{\kappa_{i}}^{y}=d]\Rightarrow\big{(}\widehat{\varphi}^{y,P}\wedge\bigwedge_{(y,y^{\prime})\in E}[\overline{\kappa_{i}}^{y^{\prime}}<d]\big{)}\Big{)}\Big{]}$$

$${\Phi }_k$$

$${\Psi }_k$$

$${\Phi }_k^g$$

$${\Psi }_k^g$$

$$\Phi_{\textsf{win}}^{J}\;=\;\exists m.\Big{(}\text{{A}}\text{{G}}\big{(}t_{J}\>\Rightarrow\>\text{{E}}\text{{X}}m\big{)}\;\wedge\;\text{{A}}\text{{F}}\big{(}w_{J}\vee(\text{int}\wedge\neg m)\big{)}\Big{)}$$

$$\Phi_{\textsf{res}}\;=\;\exists^{1}c_{1}\ldots\exists^{1}c_{k}\>\text{{A}}\text{{G}}\Big{(}(\!\!\bigvee_{1\leq i\leq k}\!\!c_{i})\vee\text{{E}}\text{{X}}\Big{(}(\!\!\bigvee_{1\leq i\leq k}\!\!c_{i})\vee\Big{(}\ldots\vee\text{{E}}\text{{X}}(\!\!\bigvee_{1\leq i\leq k}\!\!c_{i})\Big{)}\Big{)}\Big{)}$$

Full text

1 Introduction

Temporal logics have been introduced in computer science in the late 1970’s [14]; they provide a powerful formalism for specifying correctness properties of evolving systems. Various kinds of temporal logics have been defined, with different expressiveness and algorithmic properties. For instance, the Computation Tree Logic ($\mathsf{CTL}$) expresses properties of the computation tree of the system under study (time is branching : a state may have several successors), and the Linear-time Temporal Logic ($\mathsf{LTL}$) expresses properties of one execution at a time (a system is viewed as a set of executions).

Temporal logics allow model checking, i.e. the automatic verification that a finite state system satisfies its expected behavioral specifications [15, 3]. It is well known that $\mathsf{CTL}$ model-checking is PTIME-complete and $\mathsf{LTL}$ model-checking (based on automata techniques) is PSPACE-complete. But verification tools exist for both logics and model-checking is now commonly used in the design of critical reactive systems. The main limitation to this approach is the state-explosion problem : symbolic techniques (for example with BDD), SAT-based approaches, or partial order reductions have been developed and they are impressively successful. The SAT-based model-checking consists in using SAT-solvers in the decision procedures. It was first developed for bounded model-checking (to search for executions whose length is bounded by some integer, satisfying some temporal property) which can be reduced to some satisfiability problem and then can be solved by a SAT-solver [2]. SAT approaches have also been extended to unbounded verification and combined with other techniques [12]. Many studies have been done in this area, and it is widely considered as an important approach in practice, which complements other symbolic techniques like BDD (see [1] for a survey).

In terms of expressiveness, $\mathsf{CTL}$ (or $\mathsf{LTL}$) still has some limitations : in particular, it lacks the ability of counting. For instance, it cannot express that an event occurs (at least) at every even position along a path, or that a state has two successors. In order to cope with this, temporal logics have been extended with propositional quantifiers [16] : those quantifiers allow for adding fresh atomic propositions in the model before evaluating the truth value of a temporal-logic formula. That a state has at least two successors can then be expressed (in quantified $\mathsf{CTL}$, hereafter written $\mathsf{QCTL}$) by saying that it is possible to label the model with atomic proposition $p$ in such a way that there is a successor that is labelled with $p$ and one that is not.

Different semantics for $\mathsf{QCTL}$ have been studied in literature depending on the definition of the labelling : either it refers to the finite-state model – it is the structure semantics – or it refers to the execution tree – it is the tree semantics. Both semantics are interesting and have been extensively studied [9, 7, 13, 8, 4, 10]. While the tree semantics allow us to use the tree automata techniques to get decision procedures (model-checking and satisfiability are TOWER-complete [10]), the situation is quite different for the structure semantics : in this framework, model-checking is PSPACE-complete and satisfiability is undecidable [7].

In this paper, we focus on the structure semantics, and we propose a model-checking algorithm based on a reduction to $\mathsf{QBF}$ : given a Kripke structure $\mathcal{K}$ and a $\mathsf{QCTL}$ formula $\Phi$, we show how to build a $\mathsf{QBF}$ formula $\widehat{\Phi}^{\mathcal{K}}$ which is valid iff $\mathcal{K}\models\Phi$. It is natural to use $\mathsf{QBF}$  quantifiers to deal with propositional quantifiers of $\mathsf{QCTL}$. Of course, $\mathsf{QBF}$-solvers are not as efficient as SAT-solvers, but still much progress has been made (and $\mathsf{QBF}$-solvers have already been considered for model-checking, as in [6]). We propose several reductions depending on the way of dealing with nested temporal modalities, and we have implemented a prototype (based on Z3 SMT-solver [5]) to compare these reductions over several examples. As far as we know, it is the first implementation of a model-checker for $\mathsf{QCTL}$.

Here, our first objective is to use the $\mathsf{QBF}$-solver as a tool to check complex properties over limited size models, and this is therefore different from the classical use of $\mathsf{SAT}$-based techniques which are precisely applied to solve verification problems for very large systems.

The outline of the paper is as follows : we begin with setting up the necessary formalism in order to define $\mathsf{QCTL}$. We then devote Section 3 to the different reductions to $\mathsf{QBF}$. Finally, Section 4 contains several practical results and examples.

2 Definitions

2.1 Kripke structures

Let $\mathsf{AP}$ be a set of atomic propositions.

Definition 2.1**.**

A Kripke structure is a tuple $\mathcal{K}=\langle V,E,\ell\rangle$, where $V$ is a finite set of vertices (or states), $E\subseteq V\times V$ is a set of edges (we assume that for any $v\in V$, there exists $v^{\prime}\in V$ s.t. $(v,v^{\prime})\in E$), and $\ell\colon V\to 2^{\mathsf{AP}}$ is a labelling function.

An infinite path (also called an execution) in a Kripke structure is an infinite sequence $\rho=x_{0}x_{1}x_{2}\ldots$ such that for any $i$ we have $x_{i}\in V$ and $(x_{i},x_{i+1})\in E$. We write $\mathsf{Path}^{\omega}_{\mathcal{K}}$ for the set of infinite paths of $\mathcal{K}$ and $\mathsf{Path}^{\omega}_{\mathcal{K}}(x)$ for the set of infinite paths issued from $x\in V$. Given such a path $\rho$, we use $\rho_{\leq i}$ to denote the $i$-th prefix $x_{0}\ldots x_{i}$, $\rho_{\geq i}$ for the $i$-th suffix $x_{i}x_{i+1}\ldots$, and $\rho(i)$ for the vertex $x_{i}$. The size of $\mathcal{K}$ is $|V|+|E|$.

Given a set $P\subseteq\mathsf{AP}$, two Kripke structures $\mathcal{K}=(V,E,\ell)$ and $\mathcal{K}^{\prime}=(V^{\prime},E^{\prime},\ell^{\prime})$ are said $P$-equivalent (denoted by $\mathcal{K}\equiv_{P}\mathcal{K}^{\prime}$) if $V=V^{\prime}$, $E=E^{\prime}$, and for every $x\in V$ we have : $\ell(x)\cap P=\ell^{\prime}(x)\cap P$.

2.2 $\mathsf{QCTL}$

This section is devoted to the definition of the logic $\mathsf{QCTL}$, which extends the classical branching-time temporal logic $\mathsf{CTL}$ with quantifications over atomic propositions.

Definition 2.2**.**

The syntax of $\mathsf{QCTL}$ is defined by the following grammar :

[TABLE]

where $q$ and $p$ range over $\mathsf{AP}$.

$\mathsf{QCTL}$  formulas are evaluated over states of Kripke structures :

Definition 2.3**.**

Let $\mathcal{K}=\langle V,E,\ell\rangle$ be a Kripke structure, and $x\in V$. The semantics of $\mathsf{QCTL}$ formulas is defined inductively as follows :

[TABLE]

In the sequel, we use standard abbreviations such as $\top$, $\bot$, $\wedge$, $\Rightarrow$ and $\Leftrightarrow$. We also use the additional (classical) temporal modalities of $\mathsf{CTL}$ : $\text{{A}}\text{{X}}\varphi=\neg\text{{E}}\text{{X}}\neg\varphi$ , $\text{{E}}\text{{F}}\varphi=\text{{E}}\top\text{{U}}\varphi$, $\text{{A}}\text{{F}}\varphi=\text{{A}}\top\text{{U}}\varphi$, $\text{{E}}\text{{G}}\varphi=\neg\text{{A}}\text{{F}}\neg\varphi$, $\text{{A}}\text{{G}}\varphi=\neg\text{{E}}\text{{F}}\neg\varphi$, $\text{{E}}\varphi\text{{W}}\psi=\neg\text{{A}}\neg\psi\text{{U}}(\neg\psi\wedge\neg\varphi)$ and $\text{{A}}\varphi\text{{W}}\psi=\neg\text{{E}}\neg\psi\text{{U}}(\neg\psi\wedge\neg\varphi)$.

Moreover, we use the following abbreviations related to quantifiers over atomic propositions : $\forall p.\ \varphi=\neg\exists p.\ \neg\varphi$, and for a set $P=\{p_{1},\ldots,p_{k}\}\subseteq\mathsf{AP}$, we write $\exists P.\varphi$ for $\exists p_{1}.\ldots\exists p_{k}.\varphi$ and $\forall P.\varphi$ for $\forall p_{1}.\ldots\forall p_{k}.\varphi$.

The size of a formula $\varphi\in\mathsf{QCTL}$, denoted $|\varphi|$, is defined inductively by : $|q|=1$, $|\neg\varphi|=|\exists p.\varphi|=|\text{{E}}\text{{X}}\varphi|=1+|\varphi|$, $|\varphi\vee\psi|=|\text{{E}}\varphi\text{{U}}\psi|=|\text{{A}}\varphi\text{{U}}\psi|=1+|\varphi|+|\psi|$. Moreover we use $\mathsf{ht}(\varphi)$ to denote the temporal height of $\varphi$, that is the maximal number of nested temporal modalities in $\varphi$. And given a subformula $\psi$ in $\Phi$, the temporal depth of $\psi$ in $\Phi$ (denoted $\mathsf{td}_{\Phi}(\psi)$) is the number of temporal modalities having $\varphi$ in their scope.

In the following, we denote by $\mathsf{SubF}(\Phi)$ (resp. $\mathsf{SubTF}(\Phi)$) the set of subformulas of $\Phi$ (resp. the set of subformulas starting with a temporal modality).

Two $\mathsf{QCTL}$ formulas $\varphi$ and $\psi$ are said to be equivalent (written $\varphi\equiv\psi$) iff for any structure $\mathcal{K}$, any state $x$, we have $\mathcal{K},x\models\varphi$ iff $\mathcal{K},x\models\psi$. This equivalence is substitutive.

Discussion on the semantics.

The semantics we defined is classically called the structure semantics : a formula $\exists p.\varphi$ holds true in a Kripke structure $\mathcal{K}$ iff there exists a $p$-labeling of the structure $\mathcal{K}$ such that $\varphi$ is satisfied. Another well-known semantics coexists in the literature for propositional quantifiers, the tree semantics : $\exists p.\ \varphi$ holds true when there exists a $p$-labelling of the execution tree (the infinite unfolding) of the Kripke structure under which $\varphi$ holds. If, for $\mathsf{CTL}$, interpreting formulas over the structure or the execution tree is equivalent, this is not the case for $\mathsf{QCTL}$. Moreover, these two semantics do not have the same algorithmic properties : if $\mathsf{QCTL}$ model-checking and satisfiability are TOWER-complete for the tree semantics (the algorithms are based on tree automata techniques), $\mathsf{QCTL}$ model-checking is PSPACE-complete for the structure semantics but satisfiability is undecidable. (see [10] for a survey). Nevertheless, in both semantics, $\mathsf{QCTL}$ and $\mathsf{QCTL}^{*}$ (the extension of $\mathsf{CTL}^{*}$ with quantifications) are equally expressive, and are as expressive 111This requires adequate definitions, since a temporal logic formula may only deal with the reachable part of the model, while $\mathsf{MSO}$ has a more global point of view. as the Monadic Second-Order Logic over the finite structure or the infinite trees (depending on the semantics). Note also that any $\mathsf{QCTL}$ formula is equivalent to a formula in Prenex normal form (we will use this result in next sections).

Finally, there is also the amorphous semantics [7], where $\exists p.\ \varphi$ holds true at a state $s$ in some Kripke structure $\mathcal{K}$ if, and only if, there exists some Kripke structure $\mathcal{K}^{\prime}$ with a state $s^{\prime}$ such that $s$ and $s^{\prime}$ are bisimilar, and for which there exists a $p$-labeling making $\varphi$ hold true at $s^{\prime}$. With these semantics, the logic is insensitive to unwinding, and more generally it is bisimulation-invariant (contrary to the two previous semantics, see below).

2.3 Examples of $\mathsf{QCTL}$ formulas

$\mathsf{QCTL}$ allows us to express complex properties over Kripke structures : for example, it is easy to build a characteristic formula (up to isomorphism) of a structure, and one can also reduce model-checking problems for multi-player games to $\mathsf{QCTL}$ model-checking [11]…Below, we give several examples of counting properties, to illustrate the expressive power of propositional quantifiers.

The first one of the formulas below expresses that there exists a unique reachable state verifying $\varphi$, and the second one states that there exists a unique immediate successor satisfying $\varphi$ :

[TABLE]

where we assume that $p$ does not appear in $\varphi$. Consider the formula 1: if there were two reachable states satisfying $\varphi$, then labelling only one of them with $p$ would falsify the A****G subformula. For 2, the argument is similar.

The existence of at least $k$ successors satisfying a given property can be expressed with :

[TABLE]

And we can define $\text{{E}}_{=k}\text{{X}}\varphi$ as to $\text{{E}}_{\geq k}\text{{X}}\varphi\>\wedge\>\neg\text{{E}}_{\geq k+1}\text{{X}}\varphi$. Note that these examples show why $\mathsf{QCTL}$ formulas are not bisimulation-invariant.

When using $\mathsf{QCTL}$ to specify properties, one often needs to quantify (existentially or universally) over one reachable state we want to mark with a given atomic proposition. To this aim, we add the following abbreviations :

[TABLE]

3 Model-checking QCTL

Model-checking $\mathsf{QCTL}$ is a PSPACE-complete problem (for detailed results about program complexity and formula complexity, see [10]), and it is NP-complete for the restricted set of formulas of the form $\exists P.\varphi$, with $P\subseteq\mathsf{AP}$ and $\varphi\in\mathsf{CTL}$[9]. In this section, we give a reduction from the $\mathsf{QCTL}$ model-checking problem to $\mathsf{QBF}$.

In the following, we assume a Kripke structure $\mathcal{K}=\langle V,E,\ell\rangle$, an initial state $x_{0}\in V$ and a $\mathsf{QCTL}$ formula $\Phi$ to be fixed. Let $V$ be $\{v_{1},\ldots,v_{n}\}$. We also assume w.l.o.g.  that every quantifier $\exists$ and $\forall$ in $\Phi$ introduces a fresh atomic proposition, and distinct from the propositions used in $\mathcal{K}$. We use $\mathsf{AP}_{Q}^{\Phi}$ to denote the set of quantified atomic propositions in $\Phi$.

These assumptions allow us to use an alternative notation for the semantics of $\Phi$-subformulas : the truth value of $\varphi$ will be defined for a state $x$ in $\mathcal{K}$ within an environment $\varepsilon:\mathsf{AP}_{Q}^{\Phi}\mapsto 2^{V}$, that is a partial mapping associating a subset of vertices to a proposition in $\mathsf{AP}_{Q}^{\Phi}$. We use $\mathcal{K},x\models_{\varepsilon}\varphi$ to denote that $\varphi$ holds at $x$ in $\mathcal{K}$ within $\varepsilon$. This ensures that the $\mathcal{K}$’s labelling $\ell$ is not modified when a subformula is evaluated, only $\varepsilon$ is extended with labellings for new quantified propositions. Formally the main changes of the semantics are as follows :

[TABLE]

where $\varepsilon[p\mapsto V^{\prime}]$ denotes the mapping which coincides with $\varepsilon$ for every proposition in $AP_{Q}^{\Phi}\setminus\{p\}$ and associates $V^{\prime}$ to $p$.

We use this new notation in order to better distinguish initial $\mathcal{K}$’s propositions and quantified propositions to make proofs simpler. Of course, there is no semantic difference : $\mathcal{K},x\models\Phi$ iff $\mathcal{K},x\models_{\emptyset}\Phi$.

In next sections, we consider general quantified propositional formulas ($\mathsf{QBF}$) of the form :

[TABLE]

The formal semantics of a formula $\alpha$ is defined over a Boolean valuation for free variables in $\alpha$ (i.e. propositions which are not bounded by a quantifier 222We assume w.l.o.g. that every quantifier $\exists$ and $\forall$ introduces a new proposition.), and it is defined as usual. A formula is said to be closed when it does not contain free variables. In the following, we use the standard notion of validity for closed $\mathsf{QBF}$ formulas.

Our aim is then to build a (closed) $\mathsf{QBF}$ formula $\widehat{\Phi}^{x_{0}}$ such that $\widehat{\Phi}^{x_{0}}$ is valid iff $\Phi$ holds true at $x_{0}$ in $\mathcal{K}$.

3.1 Overview

We present several reductions of $\mathsf{QCTL}$ model-checking problem to $\mathsf{QBF}$ validity problem. Given a $\Phi$-subformula $\varphi$, a vertex $x\in V$, and a subset $P\subseteq AP_{Q}^{\Phi}$, we define a $\mathsf{QBF}$ formula $\widehat{\varphi}^{x,P}$ whose variables belongs to $\mathsf{AP}_{Q}^{\Phi}\times V$ (in the following, we use the notation $p^{x}$ for $p\in\mathsf{AP}_{Q}^{\Phi}$ and $x\in V$). The first two reductions are based on different encodings of temporal modalities, but share a common part given at Table 1.

3.1.1 Unfolding characterization of the until operators

First, we can complete previous construction rules of Table 1 with those of Table 2 to get the first method (called UU). This is a naive approach consisting in encoding the temporal modalities as unfoldings of the transition relation.

Before stating the correctness of the construction, we need to associate a Boolean valuation $v_{\varepsilon}$ for variables in $\mathsf{AP}_{Q}^{\Phi}\times V$ to an environment $\varepsilon$ for $\mathsf{AP}_{Q}^{\Phi}$. We define $v_{\varepsilon}$ as follows : for any $p\in\mathsf{AP}_{Q}^{\Phi}$ and $x\in V$, $v_{\varepsilon}(p^{x})=\top$ iff $x\in\varepsilon(p)$.

Now we have the following theorem whose proof is in appendix A :

Theorem 3.1**.**

Given a $\mathsf{QCTL}$ formula $\Phi$, a Kripke structure $\mathcal{K}=\langle V,E,\ell\rangle$, a state $x\in V$, an environment $\varepsilon:\mathsf{AP}_{Q}^{\Phi}\mapsto 2^{V}$ and a $\Phi$-subformula $\varphi$, if $\widehat{\varphi}^{x,\mathsf{dom}(\varepsilon)}$ is defined inductively w.r.t. the rules of Tables 1 and 2, we have: $\mathcal{K},x\models_{\varepsilon}\varphi\quad\mbox{iff}\quad v_{\varepsilon}\models\widehat{\varphi}^{x,\mathsf{dom}(\varepsilon)}$

It remains to define $\widehat{\Phi}^{x}$ as $\widehat{\Phi}^{x,\emptyset}$ and we get the reduction : $\mathcal{K},x_{0}\models\Phi$ iff $\widehat{\Phi}^{x_{0}}$ is valid.

The main drawback of this reduction is the size of the $\mathsf{QBF}$ formula : indeed any Until modality may induce a formula whose size is in $O(|V|!)$, and the size of the resulting formula $\widehat{\Phi}^{x_{0}}$ is then in $O((|\Phi|\cdot|V|!)^{\mathsf{ht}(\Phi)})$. Nevertheless, one can notice that the reduction does not use new quantified propositons to encode the temporal modalities, contrary to other methods we will see later.

3.2 Fixed point characterization of the until operators

Here we present the fixed point method (called FP) for dealing with the modalities A****U and E****U. Let $\varphi$ and $\psi$ be two $\mathsf{QCTL}$-formulas. The idea of the method is to build a $\mathsf{QCTL}$  formula that is equivalent to $\text{{E}}\varphi\text{{U}}\psi$ (or $\text{{A}}\varphi\text{{U}}\psi$), using only the modalities E****X, A****X and A****G.

We first have the following lemma :

Lemma 3.2**.**

For any $\mathsf{QCTL}$ formula $\text{{E}}\varphi\text{{U}}\psi$, we have :

[TABLE]

Proof 3.3**.**

*Let $x$ be a state in a Kripke structure $\mathcal{K}$. Let $\theta$ be the formula \big{(}\text{{A}}\text{{G}}\big{(}z\Leftrightarrow(\psi\vee(\varphi\wedge\text{{E}}\text{{X}}\>z))\big{)}\;\Rightarrow\;z\big{)}.

Assume $\mathcal{K},x\models\text{{E}}\varphi\text{{U}}\psi$. We can use the standard characterization of E****U as fixed point : $x$ belongs to the least fixed point of the equation $Z=\psi\vee(\varphi\wedge\text{{E}}\text{{X}}\>Z)$ where $\psi$ (resp. $\varphi$) is here interpreted as the set of states satisfying $\psi$ (resp. $\varphi$). Therefore any $z$-labelling of reachable states from $x$ 333Labelling other states does not matter. corresponding to a fixed point will have the state $x$ labelled. This is precisely what is specified by the $\mathsf{QCTL}$ formula.

Now if $\mathcal{K},x\models\theta$ for every $z$-labelling corresponding to a fixed point of the previous equation, this is the case for the $z$-labelling of the states reachable from $x$ and satisfying $\text{{E}}\varphi\text{{U}}\psi$, and we deduce $\mathcal{K},x\models\text{{E}}\varphi\text{{U}}\psi$.*

And we have the same result for A****U :

Lemma 3.4**.**

For any $\mathsf{QCTL}$ formula $\text{{A}}\varphi\text{{U}}\psi$, we have :

[TABLE]

Proof 3.5**.**

Similar to the proof of Lemma 3.2

As a direct consequence, we get the following result :

Proposition 3.6**.**

For any $\mathsf{QCTL}$ formula $\Phi$, we can build an equivalent $\mathsf{QCTL}$ formula $\mathsf{fpc}(\Phi)$ such that : (1) $\mathsf{fpc}(\Phi)$ is built up from atomic propositions, Boolean operators, propositional quantifiers and modalities **EX and **AG, and (2) the size of $\mathsf{fpc}(\Phi)$ is linear in $|\Phi|$.

Note that the size of $\mathsf{fpc}(\Phi)$ comes from the fact that there is no duplication of subformulas when applying the transformation rules based on equivalences of Lemmas 3.2 and 3.4. Moreover, the temporal height of $\mathsf{fpc}(\Phi)$ is $\mathsf{ht}(\Phi)+1$.

And to translate $\mathsf{fpc}(\Phi)$ into $\mathsf{QBF}$, it remains to add a single rule 444For A****X we can either change the rule for E****X with a disjunction, or express it with E****X and $\neg$. to the definitions of Table 1 to deal with A****G :

[TABLE]

And we have :

Theorem 3.7**.**

Given a $\mathsf{QCTL}$ formula $\Phi$, a Kripke structure $\mathcal{K}=\langle V,E,\ell\rangle$, a state $x\in V$ and an environment $\varepsilon:\mathsf{AP}_{Q}^{\Phi}\mapsto 2^{V}$, for any $\Phi$-subformula $\varphi$, if $\widehat{\mathsf{fpc}(\varphi)}^{x,\mathsf{dom}(\varepsilon)}$ is defined inductively w.r.t. the rules of Table 1 and the rule 8, we have :

[TABLE]

Proof 3.8**.**

The proof is a direct consequence of Proposition 3.6.

With this approach, the size of $\widehat{\mathsf{fpc}(\Phi)}^{x}$ is in $O((|\Phi|\cdot|\mathcal{K}|)^{\mathsf{ht}(\Phi)})$. Indeed, an E****U (or A****U) modality gives rise to a $\mathsf{QBF}$ formula of size $(|V|+|E|)$. The exponential size comes from the potential nesting of temporal modalities : to avoid it, one could consider the DAG-size of formulas. In the next section, we consider another solution. Note also that the number of propositional variables in the $\mathsf{QBF}$ formula is bounded by $|\mathsf{AP}_{Q}^{\Phi}|\cdot|V|$.

3.3 Reduction via flat formulas

To avoid the size explosion of $\widehat{\Phi}^{x}$, one can use an alternative approach for Prenex $\mathsf{QCTL}$ formulas. Remember that any $\mathsf{QCTL}$ formula can be translated into an equivalent $\mathsf{QCTL}$ formula in Prenex normal form whose size is linear in the size of the original formula [10].

In the following, a $\mathsf{CTL}$ formula is said to be basic when it is of the form $\text{{E}}\text{{X}}\alpha$, $\text{{E}}\alpha\text{{U}}\beta$ or $\text{{A}}\alpha\text{{U}}\beta$ where $\alpha$ and $\beta$ are Boolean combinations of atomic propositions. It is easy to observe that any $\mathsf{CTL}$ formula can be translated into a $\mathsf{QCTL}$ formula with a temporal height less or equal to 2 :

Proposition 3.9**.**

Any $\mathsf{CTL}$ formula $\Phi$ is equivalent to some $\mathsf{QCTL}$ formula $\Psi$ of the form :

[TABLE]

where $\Phi_{0}$ is a Boolean combination of basic $\mathsf{CTL}$ formulas and every $\theta_{i}$ is a basic $\mathsf{CTL}$  formula (for any $1\leq i\leq m$). Moreover, $|\Psi|$ is in $O(|\Phi|)$.

Proof 3.10**.**

Let $S$ be the set of temporal subformulas occurring in $\Phi$ at a temporal depth greater or equal to 1. Assume $S=\{\varphi_{1},\ldots,\varphi_{m}\}$ and let $\{\kappa_{1},\ldots,\kappa_{m}\}$ be $m$ fresh atomic propositions. For any $1\leq i\leq m$, we define $\theta_{i}$ as $\varphi_{i}$ where every temporal subformula $\varphi_{j}$ at temporal depth 1 in $\varphi_{i}$, is replaced by $\kappa_{j}$. $\Phi_{0}$ is defined similarly from $\Phi$.

The equivalence $\Phi\equiv\Psi$ can be proven by induction over $|S|$. If $|S|=0$, the formula satisfies the property. Now consider a formula with $|S|=m>0$. Let $\varphi_{m}\in S$ be a basic $\mathsf{CTL}$ formula. Let $\Phi^{\prime}$ be the following formula : $\exists\kappa_{m}.(\Phi[\varphi_{m}\leftarrow\kappa_{m}]\wedge\text{{A}}\text{{G}}(\kappa_{m}\Leftrightarrow\varphi_{m}))$, where $\varphi[\alpha\leftarrow\beta]$ is $\varphi$ where every occurrence of $\alpha$ is replaced by $\beta$. Then $\Phi$ and $\Phi^{\prime}$ are equivalent : any state reachable from the current state $x$ will be labeled by $\kappa_{m}$ iff $\varphi_{m}$ holds true at that state (NB : the states that are not reachable from $x$ do not matter for the truth value of $\Phi$) and this enforces the equivalence. And then we can apply the induction hypothesis to get :

[TABLE]

Note that the last equivalence comes from the fact that no $\kappa_{i}$ with $i<m$ occurs in $\varphi_{m}$ and we also have $\theta_{m}=\varphi_{m}$. The size of $\Psi$ is linear in $|\Phi|$.

In the following, a $\mathsf{QCTL}$ formula of the form {\displaystyle\mathcal{Q}.\big{(}\Phi_{0}\wedge\bigwedge_{i=1\ldots m}\text{{A}}\text{{G}}(\kappa_{i}\Leftrightarrow\theta_{i})\big{)}}, where $\mathcal{Q}$ is a sequence of quantifications, $\Phi_{0}$ is a Boolean combination of basic $\mathsf{CTL}$ formulas, and every $\theta_{i}$ (for $i=1,\ldots,m$) is a basic $\mathsf{CTL}$ formula, is said to be a flat formula.

As a corollary of previous results, we have :

Proposition 3.11**.**

Any $\mathsf{QCTL}$ formula $\Phi$ is equivalent to some flat formula whose size is linear in $|\Phi|$.

Given a $\mathsf{QCTL}$ formula $\Phi$, we use $\mathsf{flat}(\Phi)$ to denote the flat formula equivalent to $\Phi$, obtained by first translating $\Phi$ into Prenex normal form, and then transform the $\mathsf{CTL}$ subformula as described in Proposition 3.9.

Applying method FP to some flat formula provides a $\mathsf{QBF}$ formula of polynomial size since a flat formula has a temporal height less or equal to 2 :

Corollary 3.12**.**

Given a $\mathsf{QCTL}$ formula $\Phi$, a Kripke structure $\mathcal{K}=\langle V,E,\ell\rangle$ and a state $x$, the $\mathsf{QBF}$ formula \stackon[-8pt]$\mathsf{fpc}(\mathsf{flat}(\Phi))$\vstretch1.5\hstretch8^ x obtained by applying the rules of Table 1 and the rule 8 is valid iff $\mathcal{K},x\models\Phi$. And the size of \stackon[-8pt]{\mathsf{fpc}(\mathsf{flat}(\Phi))}{\vstretch{1.5}{\hstretch{8}{\widehat{\phantom{\;}}}}}^{x} is in $O(|V|\cdot(|V|+|E|)\cdot|\Phi|)$.

Therefore this reduction (called FFP) provides a PSPACE algorithm for $\mathsf{QCTL}$ model-checking. But there are two disadvantages of this approach. First, putting the formula into Prenex normal form may increase the number of quantified atomic propositions and the number of alternations (which is in fine linear in the number of quantifiers in the original formula)[10]. For example, when extracting a quantifier $\forall$ from some E****X modality, we need to introduce two propositions, this can be seen for the formula $\text{{E}}\text{{X}}(\forall p.(\text{{A}}\text{{X}}p\vee\text{{A}}\text{{X}}\neg p))$ which is translated as :

[TABLE]

where the proposition $z$ is used to mark a state, and $z^{\prime}$ is used to enforce that only at most one successor is labeled by $z$. Of course, these two remarks may have a strong impact on the complexity of the decision procedure. Finally, note also that the resulting $\mathsf{QBF}$ formula is not in Prenex normal form.

3.4 Variant of FFP

In the previous reduction, the modalities E****U and A****U may introduce an alternation of quantifiers : an atomic proposition $\kappa$ is introduced by an existential quantifier, and then an universal quantifier introduces a variable $z$ to encode the fixed point characterisation of U. We propose another reduction in order to avoid this alternation : for this, we will use bit vectors (instead of single Boolean values) associated with every state to encode the distance from the current state to a state satisfying the right-hand side of the Until modality.

First, we consider a $\mathsf{QCTL}$ formula $\Phi$ under negation normal form (NNF), where the negation is only applied to atomic propositions. This transformation makes that $\Phi$ is built from temporal modalities in $S_{tmod}=\{\text{{E}}\text{{X}},\text{{A}}\text{{X}},\text{{E}}\text{{U}},\text{{A}}\text{{U}},\text{{E}}\text{{W}},\text{{A}}\text{{W}}\}$

We can then reformulate Proposition 3.11 as follows :

Proposition 3.13**.**

Any $\mathsf{QCTL}$ formula $\Phi$ is equivalent to some $\mathsf{QCTL}$ formula $\Psi$ in NNF of the form : {\displaystyle\Psi=\mathcal{Q}\>\exists\{\kappa_{1}\ldots\kappa_{m}\}.\Big{(}\Phi_{0}\wedge\bigwedge_{i=1\ldots m}\text{{A}}\text{{G}}(\kappa_{i}\Rightarrow\theta_{i})\Big{)}} where $\mathcal{Q}$ is a sequence of quantifications, $\Phi_{0}$ is a $\mathsf{CTL}$ formula containing only the temporal modalities **EX, **AX or **AG and whose temporal height is less or equal to 1, and every $\theta_{i}$ is a basic $\mathsf{CTL}$ formula (with $1\leq i\leq m$). Moreover, $|\Psi|$ is in $O(|\Phi|)$.

Proof 3.14**.**

Consider w.l.o.g. a $\mathsf{QCTL}$ formula $\Phi$ in Prenex normal form and NNF. We can define $\Phi_{0}$ and the basic formulas $\theta_{i}$s approximately as in Proposition 3.9, except that $\Phi_{0}$ contains only **EX, **AX or **AG modalities, and every other modality gives rise to some quantified proposition $\kappa$ and a subformula $\text{{A}}\text{{G}}(\ldots)$ in the main cunjunction of $\Psi$. Every $\theta_{i}$ starts with a modality in $S_{tmod}$. Let $\varphi_{i}$ be the original $\Phi$-subformula associated with $\theta_{i}$. Note that $\Psi$ is in NNF, and $\kappa_{i}$ occurs only once in $\Psi$ in the scope of a negation, and it happens in the subformula $\text{{A}}\text{{G}}(\kappa_{i}\Rightarrow\theta_{i})$. We now have to show that $\Phi$ is equivalent to $\Psi$. Consider the formula $\widetilde{\Psi}$ where every $\Rightarrow$ is replaced by $\Leftrightarrow$ : by following the same arguments of Proposition 3.9, we clearly have $\Phi\equiv\widetilde{\Psi}$, and $\widetilde{\Psi}\Rightarrow\Psi$. It remains to prove the opposite direction.

To prove $\Psi\Rightarrow\widetilde{\Psi}$, it is sufficient to show that this is true for the empty $\mathcal{Q}$ (as equivalence is substitutive). Assume $\mathcal{K},x\models_{\varepsilon}\Psi$. Then there exists an environment $\varepsilon^{\prime}$ from $\{\kappa_{1},\ldots,\kappa_{m}\}$ to $2^{V}$ such that $\mathcal{K},x\models_{\varepsilon\circ\varepsilon^{\prime}}\Phi_{0}\wedge\bigwedge_{i}\text{{A}}\text{{G}}(\kappa_{i}\Rightarrow\theta_{i})$. Now we have :

[TABLE]

Indeed, assume that it is not true and $\mathcal{K},x\models_{\varepsilon\circ\varepsilon^{\prime}}\theta_{i}$ and $\mathcal{K},x\not\models_{\varepsilon^{\prime}}\varphi_{i}$. Consider such a formula $\varphi_{i}$ with the smallest temporal height. The only atomic propositions $\kappa_{j}$ occurring in $\theta_{i}$ are then associated with some $\theta_{j}$ and $\varphi_{j}$ which verify the property and thus any state satisfying such a $\theta_{j}$, also satisfies $\varphi_{j}$. Therefore any state labeled by such a $\kappa_{j}$ is correctly labeled (and satisfies $\varphi_{j}$). And the states that are not labeled by $\kappa_{j}$ cannot make $\theta_{i}$ to be wrongly evaluated to true (because $\kappa_{j}$ is not in the scope of a negation). Therefore $\varphi_{i}$ holds true at $x$. The same holds for $\Phi_{0}$ and $\widetilde{\Phi_{0}}$. As a direct consequence, we have $\Psi\Rightarrow\widetilde{\Psi}$.

From the previous proposition, we derive a new reduction to $\mathsf{QBF}$ (called FBV). For modalities E****W and A****W, we use the same encoding as for method FP, except that we use the corresponding Boolean proposition $\kappa_{i}$ directly for the greatest fixed point. And for Until-based modalities, corresponding to least fixed points, we will use bit vectors instead of atomic propositions to encode the truth value of E****U or A****U : for a formula $\theta_{i}=\text{{E}}\varphi\text{{U}}\psi$, we will consider a bit vector $\overline{\kappa_{i}}$ of length $\lceil\log(|V|+1)\rceil$ for every state instead of a single Boolean value $\kappa_{i}$. The idea is that in a state $x$, the value $\overline{\kappa_{i}}$ encodes in binary the distance (in terms of number of transitions) from $x$ to a state satisfying $\psi$ along a path satisfying $\varphi$. And for $\theta_{i}=\text{{A}}\varphi\text{{U}}\psi$, the value $\overline{\kappa_{i}}$ encodes the maximal distance before a state satisfying $\psi$ (along a path where $\varphi$ is true). In the following, such a $\kappa_{i}$ associated to a $\theta_{i}$ based on an Until is called an Until-$\kappa$. Note that given a bit vector $\overline{\kappa_{i}}$ and an integer value $d$ encoded in binary, we will use $[\overline{\kappa_{i}}^{y}=d]$ and $[\overline{\kappa_{i}}^{y}<d]$ to denote the corresponding propositional formulas over $\overline{\kappa_{i}}^{y}$.

The new reduction is based on the rewriting rules of Table 3 for several operators, and we define the reduction for $\text{{A}}\text{{G}}(\kappa_{i}\Rightarrow\theta_{i})$ for $\theta_{i}=\text{{E}}\varphi\text{{W}}\psi$ or $\theta_{i}=\text{{A}}\varphi\text{{W}}\psi$ as follows :

[TABLE]

And for $\text{{A}}\text{{G}}(\kappa_{i}\Rightarrow\theta_{i})$ with $\theta_{i}=\text{{E}}\varphi\text{{U}}\psi$ or $\theta_{i}=\text{{A}}\varphi\text{{U}}\psi$, we have :

[TABLE]

where $[\overline{\kappa_{i}}^{y}=d]$ and $[\overline{\kappa_{i}}^{y}<d]$ with a given value $d$ correspond to propositional formulas over $\overline{\kappa_{i}}^{y}$. And for $\text{{A}}\text{{G}}(\kappa_{i}\Rightarrow\theta_{i})$ with $\theta_{i}=\text{{A}}\varphi\text{{U}}\psi$, we have :

[TABLE]

Note that in the equivalences 11 and 12, we cannot replace the implication by an equivalence : for a state $y$ s.t. $\widehat{\varphi}^{y,P}$, the existence of some successor $y^{\prime}$ s.t. $[\overline{\kappa_{i}}^{y^{\prime}}<d]$ is not sufficient to imply $[\overline{\kappa_{i}}^{y}=d]$. This is why we consider only implications here.

Method FBV  is defined from previous rules and we get a Prenex $\mathsf{QBF}$  formula :

Corollary 3.15**.**

Given a $\mathsf{QCTL}$ formula $\Phi$, a Kripke structure $\mathcal{K}=\langle V,E,\ell\rangle$, and a state $x$, the Prenex $\mathsf{QBF}$ formula $\widehat{\mathsf{flat}(\Phi)}^{x}$ obtained by applying the rules of Tables 3 and rules 9, 10, 11, and 12 above, is valid iff $\mathcal{K},x\models\Phi$, and $|\widehat{\mathsf{flat}(\Phi)}^{x}|$ is in $O(|V|\cdot(|V|+|E|)\cdot|\Phi|)$.

This approach allows us to easily adapt the algorithm to bounded model-checking : instead of considering values from $1$ to $|V|$ for $d$ in the definition of Until modalities, one can restrict the range to a smaller interval, to get a smaller $\mathsf{QBF}$ formula to check. Note also that obtaining a Prenex $\mathsf{QBF}$ formula is interesting in practice, because many $\mathsf{QBF}$-solvers require Prenex formulas as inputs.

We can also observe that this reduction proceeds a bit like the classical model-checking algorithm for $\mathsf{CTL}$ where for deciding $x\models\Phi$, the truth value of every $\Phi$-subformula is computed in every state of the model. In some case, this may induce additional work compared to methods like FP or UU (for example to decide whether the initial state satisfies a E****U formula).

3.4.1 Using BitVectors for $\exists^{1}$ and $\forall^{1}$.

The quantifiers $\exists^{1}$ and $\forall^{1}$ are very useful in many specifications. It can be interesting to develop ad-hoc algorithms in order to improve the generated $\mathsf{QBF}$ formulas. For the first methods we described, they are translated into propositional formulas (instead of introducing extra quantified atomic propositions as they are formally defined). Another method consists in using bit vectors as in the treatment of Until modalities described above : in this case, these quantifiers introduce a unique bit vector of size $\lceil\log(|V|+1)\rceil$ to store the number of the state selected by the quantifier (that is the state which will be labeled by the proposition). This method is interesting, since it reduces the number of quantified propositions, it is integrated in the method FBV.

4 Experimental results

In this section, we consider three examples to illustrate the $\mathsf{QBF}$-based model-checking approach for $\mathsf{QCTL}$. We propose these problems because the size of the structures can easily be scaled up, and the properties to be checked are quite different. Note that these properties cannot be expressed with classical temporal logics.

We have implemented a prototype to try the different reduction strategies 555NB: For reductions FFP and FBV the formula has to be given in Prenex normal form. . Our tool is available online 666https://www.irif.fr/~francoisl/qctlmc.html : given a Kripke structure $\mathcal{K}$ with a state $x$ and a formula $\Phi$, it produces a specification file (corresponding to $\widehat{\Phi}^{x}$) for the SMT-solver Z3 [5]. The choice of Z3 was motivated by the fact that the generated $\mathsf{QBF}$ formulas are not always Prenex, which many $\mathsf{QBF}$-solvers require, unlike Z3.

4.1 $k$-connectivity

Here, we consider an undirected graph, and we want to check whether there exist (at least) $k$ internally disjoint paths 777Two paths paths $src\leftrightarrow r_{1}\leftrightarrow\ldots\leftrightarrow r_{k}\leftrightarrow dest$ and $src\leftrightarrow r^{\prime}_{1}\leftrightarrow\ldots\leftrightarrow r^{\prime}_{k^{\prime}}\leftrightarrow dest$ are internally disjoint iff $r_{i}\not=r^{\prime}_{j}$ for any $1\leq i\leq k$ and $1\leq j\leq k^{\prime}$. And note that with this def., if there is an edge $(x,y)$, there exist $k$ internally disjoint paths from $x$ to $y$ for any $k$. from a vertex $x$ to some vertex $y$. A classical result in graph theory due to Menger ensures that, given two vertices $x$ and $y$ in a graph $G$, the minimum number of vertices whose deletion makes that there is no more paths between $x$ and $y$ is equal to the maximum number of internally disjoint paths between these two vertices.

We can encode these two ideas by the following $\mathsf{QCTL}$ formulas (interpreted over $x$) :

[TABLE]

$\Phi_{k}$ uses the labelling by the $p_{i}$’s to mark the internal vertices of $k$ paths between the current position and the vertex $y$. The modality E****X is used to consider only the intermediate states (and not the starting state). The formula $\Psi_{k}$ proceeds differently : the idea is to mark exactly $k-1$ states with $p_{1},\ldots,p_{k-1}$ and to verify that there still exists at least one path leading to $y$ without going through the states labeled by some $p_{i}$.

By Menger’s Theorem, we know that these formulas are equivalent over undirected graphs.

We interpret these formulas over Kripke structures $\mathcal{S}_{n,m}$ with $n\geq m$ (see Figure 1) which correspond to two kinds of grid $n\times n$ connected by $m$ edges (these edges are of the form $(q_{i,n},r_{1,i})$ or $(q_{n,i},r_{i,1})$ The initial state is $q_{0,0}$ and when evaluating $\Phi_{k}$ or $\Psi_{k}$ we assume the state $r_{n,n}$ to be labeled by $y$. In this context, we clearly have that $\Phi_{k}$ and $\Psi_{k}$ hold for true at $q_{0,0}$ iff $k\leq m$.

Detailed results are presented in Appendix B. The main lessons we can see are :

• •

Formula $\Phi_{k}$ is much more difficult to verify : the number of temporal modalities is probably one explanation. Another one for methods FP and FFP(based on the fixed point characterization of $\text{{U}}/\text{{W}}$ modalities) could be an alternation of quantifiers : in $\Phi_{k}$, there is an existential quantification over the $p_{i}$s and the E****Us introduce an universal quantification, but it is not the case for $\Psi_{k}$, where there are only universal quantifications for these reductions.

• •

The reduction FP is the most efficient : it can be used to verify models with more than two thousands states when $m$ is small. The method FFP is also rather efficient, but the flattening seems to be too costly for such a simple formula.

• •

The reduction UU produces very large $\mathsf{QBF}$ formulas, but rather simple to check.

We can generalise the problem by verifying that there exist at least $k$ internally disjoint paths between any pair of reachable vertices $x$ and $y$ in a given structure. These previous formulas can be modified as follows :

[TABLE]

In that case, $\Phi^{g}_{k}$ is useless : too complex to be verified. And the method FP is still the most efficient.

4.2 Nim game

Nim game is a turn-based two-players game. A configuration is a set of heaps of objects and a boolean value indicating whose turn it is. At each turn, a player has to choose one non-empty heap and remove at least one object from it. The aim of each player is to remove the last object. Given a configuration $c$ and a Player-$J$ with $J\in\{1,2\}$, we can build a finite Kripke structure $\mathcal{S}_{J}$, where $x_{c}$ is a state corresponding to the configuration $c$ ; and use a $\mathsf{QCTL}$ formula $\Phi_{\textsf{win}}^{J}$ such that $\mathcal{S},x_{c}\models\Phi_{\textsf{win}}^{J}$ iff Player-$J$ has a wining strategy from $c$. Note that there is a simple and well-known criterion over the numbers of objects in each heap to decide who has a winning strategy, but we consider this problem just because it is interesting to illustrate what kind of problem we can solve with $\mathsf{QCTL}$.

Each configuration corresponds to a state in $\mathcal{S}_{J}$. Every move for Player-$\overline{J}$ from a configuration $c$ to a configuration $c^{\prime}$ provides a transition $(x_{c},x_{c^{\prime}})$ in $\mathcal{S}_{J}$. However, a move of Player-$J$ from $c$ to $c^{\prime}$ is encoded as two transitions $x_{c}\rightarrow x_{c,c^{\prime}}\rightarrow x_{c^{\prime}}$ where $x_{c,c^{\prime}}$ is then an intermediary state we use to encode a strategy for Player-$J$ (marking $x_{c,c^{\prime}}$ by an atomic proposition will correspond to Player-$J$ choosing $c^{\prime}$ from $c$). We assume that every state $x_{c}$ is labeled by $t_{1}$ if it’s Player-$1$’s turn to play at $c$, and by $t_{2}$ otherwise. Every intermediary state $x_{c,c^{\prime}}$ is labeled by int. We also label empty configurations by $w_{1}$ or $w_{2}$, depending on which player played the last move.

Clearly, the size of $\mathcal{S}$ will depend on the number of objects in each set in the initial configuration. The formula $\Phi_{\textsf{win}}^{J}$ depends only on $J$ :

[TABLE]

This formula holds true in a state corresponding to some configuration $c$ iff there exists a labelling by $m$ such that every reachable configuration where it’s Player-$J$’s turn, has a successor labeled by $m$ (thus a possible choice to do) and every execution from the current state leads to either a winning state for Player-$J$ or a non-selected intermediary state, therefore all outcomes induced by the underlying strategy have to verify $\text{{F}}w_{J}$. Note that in this example, the Kripke structure is acyclic (except the self-loops on the ending states).

From detailed results in appendix, we can see :

• •

One can consider structures with more than 10 thousand states. Note that the number of heaps is important for the size of the model, but the maximal length of a game depends on the number of objects (and is rather small in our examples).

• •

The most efficient method is FFP (with FP).

• •

Method FBV is more efficient when we consider bounded model-checking. Note that in this case, the verification may not be complete : if the $\mathsf{QBF}$ formula is valid, the property is satisfied by the structure, otherwise, no conclusion can be done, except if we can prove that the chosen bound was big enough to be sure that there is no solution. In our case, we can easily compute the maximal bound : at each turn, a player has to pick at least one object, such a move may give rise to one transition in the model (for the opponent), or two transitions (for the player for whom we look for a strategy). Thus, if there are $n$ objects in the initial configuration, we can choose $\frac{3n}{2}$ for the bound.

4.3 Resources distribution

The last example is as follows : given a Kripke structure $\mathcal{S}$ and two integers $k$ and $d$, we aim at choosing at most $k$ states (called targets in the following) such that every reachable state (from the initial one) can reach a target in less than $d$ transitions. This problem can be encoded with the following $\mathsf{QCTL}$ formula where $d$ modalities E****X are nested :

[TABLE]

For experimental results, we consider the grid $\mathcal{K}_{n,m}$ described at Figure 2. Note that for this example, reductions UU and FP are similar because there is no Until in the formula (A****G is treated as a conjunction). From detailed results in appendix, one can see :

• •

Only small models have been successfully verified.

• •

The nesting of E****Xs operators give an advantage to the reduction based on flattening (FBV and FFP) : the size of the $\mathsf{QBF}$ formula increases more slowly.

• •

The reduction FBV is the most efficient on this example. Since there is no Until modality (except behind A****G which is treated separately), the difference with FFP is due to the encoding of $\exists_{1}$ operator with a unique bit vector in FBV, this choice seems to be more efficient in this example.

5 Conclusion

We have presented several reductions from $\mathsf{QCTL}$ model-checking to $\mathsf{QBF}$. This provides a first tool for $\mathsf{QCTL}$ model-checking. Of course, this is an ongoing-work, and many improvements, are possible : the reduction strategies are still naive and could be significantly improved, and a better understanding of $\mathsf{QBF}$-solver would also be helpful to produce more efficient formulas (we have not yet tried to normalise formulas in a specific form which is often a crucial aspect in $\mathsf{SAT}$/$\mathsf{QBF}$-solving). Still, these first results are rather interesting and encouraging. They show the importance of writing "good" $\mathsf{QCTL}$ formulas for which the solver will be able to provide a result (this problem already exists for classical temporal logics, but it is more significant here due to the complexity induced by the quantifications). The examples also show that there is no "one best strategy": it depends on the structure of the considered formula, and then offering several reduction strategies seems to be necessary in a $\mathsf{QBF}$-based model-checker for $\mathsf{QCTL}$. Finally this work is also interesting because it could easily be adapted for other logics (like Sabotage logics [17]). In the future, we plan to continue to work on reduction strategies, and to use other $\mathsf{QBF}$-solvers.

Appendix A Proof of Theorem 3.1

Proof A.1**.**

We assume $\Phi$ to be fixed and we prove the property by structural induction over $\varphi$. Boolean operators are omitted.

• •

$\varphi=p$* : if $\mathcal{K},x\models_{\varepsilon}p$, then either $p$ is a quantified proposition and it belongs to $\mathsf{dom}(\varepsilon)$ and $x$ belongs to $\varepsilon(p)$ and thus $v_{\varepsilon}\models p^{x}$ by def. of $v_{\varepsilon}$, or $p$ belongs to $\ell(x)$. In both cases we have $v_{\varepsilon}\models\widehat{p}^{x,\mathsf{dom}(\varepsilon)}$. The converse is similar.*

• •

$\varphi=\text{{E}}\text{{X}}\psi$* : $\mathcal{K},x\models_{\varepsilon}\text{{E}}\text{{X}}\psi$ iff there exists $(x,x^{\prime})\in E$ s.t. $\mathcal{K},x^{\prime}\models_{\varepsilon}\psi$, iff (by i.h.) there exists $(x,x^{\prime})\in E$ s.t.  $v_{\varepsilon}\models\widehat{\psi}^{x^{\prime},\mathsf{dom}(\varepsilon)}$ which is equivalent to $v_{\varepsilon}\models\widehat{\text{{E}}\text{{X}}\psi}^{x,\mathsf{dom}(\varepsilon)}$.*

• •

$\varphi=\exists p.\psi$. We have $\mathcal{K},x\models_{\varepsilon}\exists p.\psi$ iff there exists $V^{\prime}\subseteq V$ s.t. $\mathcal{K},x\models_{\varepsilon[p\mapsto V^{\prime}]}\psi$, iff (i.h.) $v_{\varepsilon[p\mapsto V^{\prime}]}\models\widehat{\psi}^{x,\mathsf{dom}(\varepsilon)\cup\{p\}}$ which is equivalent to $v_{\varepsilon}\models\exists p^{v_{1}}\ldots p^{v_{n}}.\widehat{\psi}^{x,\mathsf{dom}(\varepsilon)\cup\{p\}}$ (by def. of $v_{\varepsilon}$).

• •

$\varphi=\text{{E}}\psi_{1}\text{{U}}\psi_{2}$* : The definition of $\widehat{\varphi}^{x,\mathsf{dom}(\varepsilon)}$ corresponds to a finite unfolding of the expansion law that characterizes the EU modality. Assume $\mathcal{K},x\models_{\varepsilon}\varphi$. There exists a path $\rho\in\mathsf{Path}^{\omega}_{\mathcal{K}}(x)$ and a position $i\geq 0$ s.t. $\rho(i)\models_{\varepsilon}\psi_{2}$ and $\rho(k)\models_{\varepsilon}\psi_{1}$ for any $0\leq k<i$. The finite prefix $x=\rho(0)\cdots\rho(k)$ can be assumed to be simple, and then $k<|V|$. By using i.h., we get $v_{\varepsilon}\models\widehat{\psi_{2}}^{\rho(i),\mathsf{dom}(\varepsilon)}$, and $v_{\varepsilon}\models\widehat{\psi_{1}}^{\rho(k),\mathsf{dom}(\varepsilon)}$ for any $0\leq k<i$. From this point, the reader can easily verify by induction (starting at $i$, down to 0) that $v_{\varepsilon}\models\overline{\text{{E}}\psi_{1}\text{{U}}\psi_{2}}^{\rho(k),dom(\varepsilon),\{\rho(j)|j\leq k\}}$ for all $k\leq i$. This makes $\widehat{\varphi}^{x,\mathsf{dom}(\varepsilon)}$ to be satisfied by $v_{\varepsilon}$.*

Conversely, assume $v_{\varepsilon}\models\widehat{\varphi}^{x,\mathsf{dom}(\varepsilon)}$. Let us build a finite path $x=x_{0},x_{1},\cdots x_{i}$ that satisfies $\psi_{1}\text{{U}}\psi_{2}$. The first vertex is of course $x$, and we have $v_{\varepsilon}\models\overline{\text{{E}}\psi_{1}\text{{U}}\psi_{2}}^{x,dom(\varepsilon),\{x\}}$. Fix $i$ so that for every $0\leq k\leq i$, $x_{k}$ is built, $v_{\varepsilon}\models\overline{\text{{E}}\psi_{1}\text{{U}}\psi_{2}}^{x_{k},dom(\varepsilon),\{x_{j}|j\leq k\}}$, $v_{\varepsilon}\not\models\widehat{\psi_{2}}^{x_{k},dom(\varepsilon)}$, and $(x_{k},x_{k+1})\in E$ when $k<i$. Then, there must be $(x_{i},y)\in E$ so that $y\not\in\{x_{j}|j\leq i\}$, and $v_{\varepsilon}\models\overline{\text{{E}}\psi_{1}\text{{U}}\psi_{2}}^{y,dom(\varepsilon),\{x_{j}|j\leq i\}\cup\{y\}}$, so we set $x_{i+1}=y$. The sequence eventually stops, because $V$ is finite and the path is simple. If $x_{i}$ is its last vertex, then we must have $v_{\varepsilon}\models\widehat{\psi_{2}}^{x_{i},dom(\varepsilon)}$, and $v_{\varepsilon}\models\widehat{\psi_{1}}^{x_{k},dom(\varepsilon)}$ for every $0\leq k<i$. By using i.h., we get $\mathcal{K},x\models_{\varepsilon}\varphi$.

• •

$\varphi=\text{{A}}\psi_{1}\text{{U}}\psi_{2}$* : this case is similar to the previous one, except that we have to consider loops. Assume $\mathcal{K},x\models_{\varepsilon}\varphi$. Then any path issued from $x$ satisfies $\psi_{1}\text{{U}}\psi_{2}$. If $x$ contains a self-loop, then $\psi_{2}$ has to be satisfied at $x$ (this is ensured by the first case in the def. of $\widehat{\varphi}^{x,\mathsf{dom}(\varepsilon)}$). Otherwise we consider all the paths from $x$ : either there is a simple prefix witnessing $\psi_{1}\text{{U}}\psi_{2}$, or there is a loop from some point. In the latter case, one of the state in the loop has to verify $\psi_{2}$. In both cases, the definition of $\widehat{\varphi}^{x,\mathsf{dom}(\varepsilon)}$ gives the result.*

Appendix B Experimental results

Detailed results for the three examples are presented in this section. In every case, we distinguished the time required to build the $\mathsf{QBF}$ formula (the Z3 specification) and the time required to solve it. Times are given in seconds.

B.1 $k$-connectivity

[TABLE]

[TABLE]

B.2 Nim game

[TABLE]

B.3 Resources distribution

[TABLE]