CTL Model Checking in Deduction Modulo

Abstract

In this paper we give an overview of proof-search method for CTL model checking based on Deduction Modulo. Deduction Modulo is a reformulation of Predicate Logic where some axioms—possibly all—are replaced by rewrite rules. The focus of this paper is to give an encoding of temporal properties expressed in CTL, by translating the logical equivalence between temporal operators into rewrite rules. This way, the proof-search algorithms designed for Deduction Modulo, such as Resolution Modulo or Tableaux Modulo, can be used in verifying temporal properties of finite transition systems. An experimental evaluation using Resolution Modulo is presented.

K. Ji — This work is supported by the ANR-NSFC project LOCALI (NSFC 61161130530 and ANR 11 IS02 002 01).

1 Introduction

In this paper, we express Computation Tree Logic (CTL) [4] for a given finite transition system in Deduction Modulo [6, 7]. This way, the proof-search algorithms designed for Deduction Modulo, such as Resolution Modulo [2] or Tableaux Modulo [5], can be used to build proofs in CTL. Deduction Modulo is a reformulation of Predicate Logic where some axioms—possibly all—are replaced by rewrite rules. For example, the axiom $P \Leftrightarrow (Q \vee R)$ can be replaced by the rewrite rule $P \hookrightarrow (Q \vee R)$, meaning that during the proof, P can be replaced by $Q\vee R$ at any time.

The idea of translating CTL to another framework, for instance (quantified) boolean formulae [1, 14, 16], higher-order logic [12], etc., is not new. But using rewrite rules permits to avoid the explosion of the size of formulae during translation, because rewrite rules can be used on demand to unfold defined symbols. So, one of the advantages of this method is that it can express complicated verification problems succinctly. Gilles Dowek and Ying Jiang had given a way to build an axiomatic theory for a given finite model [9]. In this theory, the formulae are provable if and only if they are valid in the model. In [8], they gave a slight extension of CTL, named SCTL, where the predicates may have arbitrary arities. And they defined a special sequent calculus to write proofs in SCTL. This sequent calculus is special because it is tailored to each specific finite model M. In this way, a formula is provable in this sequent calculus if and only if it is valid in the model M. In our method, we characterize a finite model in the same way as [9], but instead of building a deduction system, the CTL formulae are taken as terms, and the logical equivalence between different CTL formulae are expressed by rewrite rules. This way, the existing automated theorem modulo provers, for instance iProver Modulo [3], can be used to do model checking directly. The experimental evaluation shows that the resolution based proof-search algorithms is feasible, and sometimes performs better than the existing solving techniques.

The rest of this paper is organized as follows. In Sect. 2 a new variant of Deduction Modulo for one-sided sequents is presented. In Sect. 3, the usual semantics of CTL is presented. Sections 4 and 5 present the new results of this paper: in Sect. 4, an alternative semantics for CTL on finite structures is given; in Sect. 5, the rewrite rules for each CTL operator are given and the soundness and completeness of this presentation of CTL is proved, using the semantics presented in the previous section. Finally in Sect. 6, experimental evaluation for the feasibility of rewrite rules using resolution modulo is presented.

2 Deduction Modulo

One-Sided Sequents. In this work, instead of using usual sequents of the form $A_1, \ldots , A_n \vdash B_1, \ldots , B_p$, we use one-sided sequents [13], where all the propositions are put on the right hand side of the sequent sign $\vdash$ and the sequent above is transformed into $\vdash \lnot A_1, \ldots , \lnot A_n, B_1, \ldots , B_p$. Moreover, implication is defined from disjunction and negation ($A \Rightarrow B$ is just an abbreviation for $\lnot A \vee B$), and negation is pushed inside the propositions using De Morgan’s laws. For each atomic proposition P we also have a dual atomic proposition $P^{\bot }$ corresponding to its negation, and the operator $\bot$ extends to all the propositions. So that the axiom rule can be formulated as

Deduction Modulo. A rewrite system is a set $\mathcal {R}$ of term and proposition rewrite rules. In this paper, only proposition rewrite rules are considered. A proposition rewrite rule is a pair of propositions $l\hookrightarrow r$, in which l is an atomic proposition and r an arbitrary proposition. For instance, $P \hookrightarrow Q\vee R$. Such a system defines a congruence $\hookrightarrow$ and the relation $\overset{*}{\hookrightarrow }$ is defined, as usual, as the reflexive-transitive closure of $\hookrightarrow$. Deduction Modulo [7] is an extension of first-order logic where axioms are replaced by rewrite rules and in a proof, a proposition can be reduced at any time. This possibility is taken into account in the formulation of Sequent Calculus Modulo in Fig. 1. For example, with the axiom $(Q \Rightarrow R) \Rightarrow P$ we can prove the sequent $R \vdash P$. This axiom is replaced by the rules $P \hookrightarrow Q^{\bot }$ and $P \hookrightarrow R$ and the sequent $R \vdash P$ is expressed as the one-sided sequent $\vdash R^{\bot }, P$. This sequent has the proof

as $P \overset{*}{\hookrightarrow }R$.

Fig. 1.

One-sided Sequent Calculus Modulo

Note that as our system is negation free, all occurrences of atomic propositions are positive. Thus, the rule $P \hookrightarrow A$ does not correspond to an equivalence $P \Leftrightarrow A$ but to an implication $A \Rightarrow P$. In other words, our one-sided presentation of Deduction Modulo is closer to Polarized Deduction Modulo [6] with positive rules only, than to the usual Deduction Modulo. The sequent $\vdash _{\mathcal {R}} \varDelta$ has a cut-free proof is represented as $\vdash ^{cf}_{\mathcal {R}} \varDelta$ has a proof.

3 Computation Tree Logic

Properties of a transition system can be specified by temporal logic propositions. Computation tree logic is a propositional branching-time temporal logic introduced by Emerson and Clarke [4] for finite state systems. Let AP be a set of atomic propositions and p ranges over AP. The set of CTL propositions $\varPhi$ over AP is defined as follows:

$$\begin{aligned} \begin{array}{lcl} &{}\varPhi ~{::}{=}&{} p~|~\lnot \varPhi ~|~\varPhi \wedge \varPhi ~|~\varPhi \vee \varPhi ~|~AX\varPhi ~|~EX\varPhi ~ |~AF\varPhi ~|~EF\varPhi ~|~AG\varPhi ~|~EG\varPhi \\ &{} &{} |~A[\varPhi U \varPhi ]~|~E[\varPhi U \varPhi ]~|~A[\varPhi R \varPhi ]~|~E[\varPhi R \varPhi ] \end{array} \end{aligned}$$

The semantics of CTL can be given using Kripke structure, which is used in model checking to represent the behavior of a system.

Definition 1

(Kripke Structure). Let AP be a set of atomic propositions. A Kripke structure M over AP is a three tuple $M = (S,\mathsf {next},\mathsf {L})$ where

• S is a finite (non-empty) set of states.

• $\mathsf {next}: S\rightarrow \mathcal {P}^+(S)$ is a function that gives each state a (non-empty) set of successors.

• $\mathsf {L}:S\rightarrow \mathcal {P}(AP)$ is a function that labels each state with a subset of AP.

An infinite path is an infinite sequence of states $\pi =\pi _0 \pi _1 \cdots$ s.t. $\forall i\ge 0$, $\pi _{i+1} \in \mathsf {next}(\pi _i)$. Note that the sequence $\pi _i\pi _{i+1}\cdots \pi _j$ is denoted as $\pi ^j_i$ and the path $\pi$ with $\pi _0=s$ is denoted as $\pi (s)$.

Definition 2

(Semantics of CTL). Let p be an atomic proposition. Let $\varphi$, $\varphi _1$, $\varphi _2$ be CTL propositions. The relation $M,s \,\models \,\varphi$ is defined as follows.

4 Alternative Semantics of CTL

In this part we present an alternative semantics of CTL using finite paths only.

Paths with the Last State Repeated (lr-Paths). A finite path is a lr-path if and only if the last state on the path occurs twice. For instance $s_0,s_1,s_0$ is a lr-path. Note that we use $\rho =\rho _0\rho _1\ldots \rho _j$ to denote a lr-path. A lr-path $\rho$ with $\rho _0=s$ is denoted as $\rho (s)$, with $\rho _i=\rho _j$ is denoted as $\rho (i,j)$. The length of a path l is expressed by $\mathsf {len}(l)$ and the concatenation of two paths $l_1$, $l_2$ is $l_1\hat{~~}l_2$.

Lemma 1

Let M be a Kripke structure.

• 1. If $\pi$ is an infinite path of M, then $\exists i\ge 0$ such that $\pi ^i_0$ is a lr-path.

• 2. If $\rho (i,j)$ is a lr-path of M, then $\rho _0^i\hat{~}(\rho _{i+1}^j)^\omega$ is an infinite path.

Proof

For Case 1, as M is finite, there exists at least one repeating state in $\pi$. If $\pi _i$ is the first state which occurs twice, then $\pi ^i_0$ is a lr-path. Case 2 is trivial.    $\square$

Lemma 2

Let M be a Kripke structure.

• 1. For the path $l=s_0,s_1,\ldots ,s_k$, there exists a finite path $l'=s'_0,s'_1,\ldots ,s'_i$ without repeating states s.t. $s'_0=s_0$, $s'_i=s_k$, and $\forall 0< j<i$, $s'_j$ is on l.

• 2. If there is a path from s to $s'$, then there exists a lr-path $\rho (s)$ s.t. $s'$ is on $\rho$.

Proof

For the first case, $l'$ can be built by deleting the cycles from l. The second case is straightforward by the first case and Lemma 1.    $\square$

Definition 3

(Alternative Semantics of CTL). Let p be an atomic proposition and $\varphi ,\varphi _1,\varphi _2$ be CTL propositions. The relation $M, s\models _a\varphi$ is defined as follows.

We now prove the equivalence of the two semantics, that is, $M, s\models \varphi$ iff $M, s\models _a\varphi$. To simplify the proofs, we use a normal form of the CTL propositions, in which all the negations appear only in front of the atomic propositions.

Negation Normal Form. A CTL proposition is in negation normal form (NNF), if the negation $\lnot$ is applied only to atomic propositions. Every CTL proposition can be transformed into an equivalent proposition of NNF using the following equivalences.

Lemma 3

Let $\varphi$ be a CTL proposition of NNF. If $M,s\models \varphi$, then $M,s\models _a\varphi$.

Proof

By induction on the structure of $\varphi$. For brevity, we just prove the two cases where $\varphi$ is $AF\varphi _1$ and $AG\varphi _1$. The full proof is in [10].

• Let $\varphi =AF\varphi _1$. We prove the contraposition. If there is a lr-path $\rho (s)(j,k)$ s.t. $\forall 0\le i<k$, $M,\rho _i\mid \!\ne \varphi _1$, then by Lemma 1, there exists an infinite path $\rho ^j_0\hat{~}(\rho ^k_{j+1})^{\omega }$, which is a counterexample of $M,s\models AF\varphi _1$. Thus for each lr-path $\rho (s)$, $\exists 0\le i<\mathsf {len}(\rho )-1$ s.t. $M,\rho _i\models \varphi _1$ holds. Then by induction hypothesis (IH), for each lr-path $\rho (s)$, $\exists 0\le i<\mathsf {len}(\rho )-1$ s.t. $M,\rho _i\models _a\varphi _1$ holds, and thus $M,s\models _a AF\varphi _1$ holds.

• Let $\varphi = AG\varphi _1$. We prove the contraposition. If there is a lr-path $\rho (s)(j,k)$ and $\exists 0\le i<k$ s.t. $M,\rho _i\mid \!\ne \varphi _1$, then by Lemma 1, there exists an infinite path $\rho ^j_0\hat{~}(\rho ^k_{j+1})^{\omega }$, which is a counterexample of $M,s\models AG\varphi _1$. Thus for each lr-path $\rho (s)(j,k)$ and $\forall 0\le i<k$, $M,\rho _i\models \varphi _1$ holds. Then by IH, for each lr-path $\rho (s)(j,k)$ and $\forall 0\le i<k$, $M,\rho _i\models _a\varphi _1$ holds, and thus $M,s\models _a AG\varphi _1$ holds.

   $\square$

Lemma 4

Let $\varphi$ be a CTL proposition of NNF. If $M, s\models _a\varphi$, then $M,s\models \varphi$.

Proof

By induction on the structure of $\varphi$. For brevity, we just prove the two cases where $\varphi$ is $AF\varphi _1$ and $AG\varphi _1$. The full proof is in [10].

• Let $\varphi = AF\varphi _1$. If there is an infinite path $\pi (s)$ s.t. $\forall j\ge 0$, $M,\pi _j\mid \!\ne _a\varphi _1$, then by Lemma 1, there exists $k\ge 0$ s.t. $\pi ^k_0$ is a lr-path, which is a counterexample of $M,s\models _a AF\varphi _1$. Thus for each infinite path $\pi (s)$, $\exists j\ge 0$ s.t. $M,\pi _j\models _a\varphi _1$ holds. Then by IH, for each infinite path $\pi (s)$, $\exists j\ge 0$ s.t. $M,\pi _j\models \varphi _1$ holds and thus $M,s\models AF\varphi _1$ holds.

• Let $\varphi =AG\varphi _1$. Assume that there exists an infinite path $\pi (s)$ and $\exists i\ge 0$, $M,\pi _i\mid \!\ne _a\varphi _1$. By Lemma 2, there exists a lr-path $\rho (s)$ s.t. $\pi _i$ is on $\rho$, which is a counterexample of $M, s\models _aAG\varphi _1$. Thus for each infinite path $\pi (s)$ and $\forall i\ge 0$, $M,\pi _i\models _a\varphi _1$ holds. Then by IH, for each infinite path $\pi (s)$ and $\forall i\ge 0$, $M,\pi _i\models \varphi _1$ holds and thus $M,s\models AG\varphi _1$ holds.

   $\square$

Theorem 1

Let $\varphi$ be a CTL proposition. $M,s\models \varphi$ iff $M,s\models _a\varphi$.

5 Rewrite Rules for CTL

The work in this section is to express CTL propositions in Deduction Modulo and prove that for a CTL proposition $\varphi$, the translation of $M,s\models _a\varphi$ is provable if and only if $M,s\models _a\varphi$ holds. So we fix such a model $M=(S,\mathsf {next}, \mathsf {L})$. As in [9], we consider a two sorted language $\mathcal {L}$, which contains

• constants $s_1,\ldots ,s_n$ for each state of M.

• predicate symbols $\varepsilon _0, \varepsilon _{\sqcap _0}, \varepsilon _{\sqcup _0}, \varepsilon _1, \varepsilon _{\sqcap _1}, \varepsilon _{\sqcup _1}$, in which the binary predicates $\varepsilon _0$, $\varepsilon _{{\sqcap }_0}$ and $\varepsilon _{{\sqcup }_0}$ apply to all the CTL propositions, while the ternary predicates $\varepsilon _1$, $\varepsilon _{{\sqcap }_1}$ and $\varepsilon _{{\sqcup }_1}$ only apply to the CTL propositions starting with the temporal connectives AG, EG, AR and ER.

• binary predicate symbols mem for the membership, r for the $\mathsf {next}$-notation.

• a constant $\mathsf {nil}$ and a binary function symbol $\mathsf {con}$.

We use x, y, z to denote the variables of the state terms, X, Y, Z to denote the class variables. A class is in fact a set of states, here we use the class theory, rather than the (monadic) second order logic, is to emphasis that this formalism is a theory and not a logic.

CTL Term. To express CTL in Deduction Modulo, firstly, we translate the CTL proposition $\varphi$ into a term $|\varphi |$ (CTL term). The translation rules are as follows:

Note that we use $\varPhi$, $\varPsi$ to denote the variables of the CTL terms. Both finite sets and finite paths are represented with the symbols $\mathsf {con}$ and $\mathsf {nil}$. For the set $S'=\{s_i,\ldots ,s_j\}$, we use $[S']$ to denote its term form $\mathsf {con}(s_i,\mathsf {con}(\ldots ,\mathsf {con}(s_j,\mathsf {nil})\ldots ))$. For the path $s^j_i=s_i,\ldots ,s_j$, its term form $\mathsf {con}(s_j,\mathsf {con}(\ldots ,\mathsf {con}(s_i,\mathsf {nil})\ldots ))$ is denoted by $[s^j_i]$.

Definition 4

(Semantics). Semantics of the propositions in $\mathcal {L}$ is as follows.

Note that when a proposition $\varepsilon _1(|\varphi |,s,[s^j_i])$ is valid in M, for instance $M \,\models \,\varepsilon _1(\mathsf {eg}(|\varphi |),s,[s^j_i])$, $EG\varphi$ may not hold on the state s.

Fig. 2.

Example of $\mathcal {L}$

Example 1

For the structure M in Fig. 2, $M\models \varepsilon _1(\mathsf {eg}({\overline{p}}),s_3,\mathsf {con}(s_2,\mathsf {con}(s_1,\mathsf {nil})))$ holds because there exists a lr-path, for instance $s_1,s_2,s_3,s_4,s_2$ such that p holds on $s_3$ and $s_4$.

The Rewrite System $\varvec{\mathcal {R}.}$ The rewrite system has three components

• 1. rules for the Kripke structure M (denoted as $\mathcal {R}_M$),

• 2. rules for the class variables (denoted as $\mathcal {R}_c$),

• 3. rules for the semantics encoding of the CTL operators (denoted as $\mathcal {R}_{CTL}$).

The Rules of $\mathcal {R}_M$ The rules of $\mathcal {R}_M$ are as follows:

• for each atomic proposition $p\in AP$ and each state $s\in S$, if $p\in \mathsf {L}(s)$, then $\varepsilon _0({\overline{p}},s)\hookrightarrow \top$ is in $\mathcal {R}_M$, otherwise $\varepsilon _0(\mathsf {not}({\overline{p}}),s)\hookrightarrow \top$ is in of $\mathcal {R}_M$.

• for each state $s\in S$, take $r(s,[\mathsf {next}(s)])\hookrightarrow \top$ as a rewrite rule of $\mathcal {R}_M$.

The Rules of $\mathcal {R}_c$ For the class variables, as the domain of the model is finite, there exists two axioms [9] $\forall x(x=x)$, and $\forall x\forall y\forall Z((x=y\vee mem(x,Z))\Rightarrow mem(x,\mathsf {con}(y,Z)))$. The rewrite rules for these axioms are $x=x\hookrightarrow \top$ and $mem(x, \mathsf {con}(y,Z)) \hookrightarrow x=y \vee mem(x,Z)$. To avoid introducing the predicate “$=$”, the rewrite rules are replaced by the rules ($\mathcal {R}_c$)

$mem(x,\mathsf {con}(x,Z))\hookrightarrow \top$ and $mem(x,\mathsf {con}(y,Z))\hookrightarrow mem(x,Z)$.

The Rules of $\mathcal {R}_{CTL}$ The rewrite rules for the predicates carrying the semantic definition of the CTL propositions, are in Fig. 3.

Fig. 3.

Rewrite Rules for CTL Connectives ($\mathcal {R}_{CTL}$)

Now we are ready to prove the main theorem. Our goal is to prove that $M\models \varepsilon _0(|\varphi |,s)$ holds if and only if $\varepsilon _0(|\varphi |,s)$ is provable in Deduction Modulo.

Lemma 5

(Soundness). For a CTL formula $\varphi$ of NNF, if the sequent $\vdash ^{cf}_{\mathcal {R}}\varepsilon _0(|\varphi |,s)$ has a proof, then $M\models \varepsilon _0(|\varphi |,s)$.

Proof

More generally, we prove that for any CTL proposition $\varphi$ of NNF,

• if $\vdash ^{cf}_{\mathcal {R}}\varepsilon _0(|\varphi |,s)$ has a proof, then $M\models \varepsilon _0(|\varphi |,s)$.

• if $\vdash ^{cf}_{\mathcal {R}}\varepsilon _{\sqcap _0}(|\varphi |,[S'])$ has a proof, then $M\models \varepsilon _{\sqcap _0}(|\varphi |,[S'])$.

• if $\vdash ^{cf}_{\mathcal {R}}\varepsilon _{\sqcup _0}(|\varphi |,[S'])$ has a proof, then $M\models \varepsilon _{\sqcup _0}(|\varphi |,[S'])$.

• if $\vdash ^{cf}_{\mathcal {R}}\varepsilon _1(|\varphi |,s,[s^j_i])$ has a proof, in which $\varphi$ is either of the form $AG\varphi _1$, $EG\varphi _1$, $A[\varphi _1 R \varphi _2]$, $E[\varphi _1 R \varphi _2]$, then $M\models \varepsilon _1(|\varphi |,s,[s^j_i])$.

• if $\vdash ^{cf}_{\mathcal {R}}\varepsilon _{\sqcap _1}(|\varphi |,[S'],[s^j_i])$ has a proof, in which $\varphi$ is either of the form $AG\varphi _1$, $A[\varphi _1 R \varphi _2]$, then $M\models \varepsilon _{\sqcap _1}(|\varphi |,[S'],[s^j_i])$.

• if $\vdash ^{cf}_{\mathcal {R}}\varepsilon _{\sqcup _1}(|\varphi |,[S'],[s^j_i])$ has a proof, in which $\varphi$ is either of the form $EG\varphi _1$, $E[\varphi _1 R \varphi _2]$, then $M\models \varepsilon _{\sqcup _1}(|\varphi |,[S'],[s^j_i])$.

By induction on the size of the proof. Consider the different case for $\varphi$, we have 18 cases (2 cases for the atomic proposition and its negation, 2 cases for $\mathsf {and}$ and $\mathsf {or}$, 10 cases for the temporal connectives $\mathsf {ax}$, $\mathsf {ex}$, $\mathsf {af}$, $\mathsf {ef}$, $\mathsf {ag}$, $\mathsf {eg}$, $\mathsf {au}$, $\mathsf {eu}$, $\mathsf {ar}$, $\mathsf {er}$, 4 cases for the predicate symbols $\varepsilon _{\sqcap _0}$, $\varepsilon _{\sqcup _0}$, $\varepsilon _{\sqcap _1}$, $\varepsilon _{\sqcup _0}$), but each case is easy. For brevity, we just prove two cases. The full proof is in [10].

• Suppose the sequent $\vdash ^{cf}_{\mathcal {R}}\varepsilon _0(\mathsf {af}(|\varphi |),s)$ has a proof. As $\varepsilon _0(\mathsf {af}(|\varphi |),s)\hookrightarrow \varepsilon _0(|\varphi |,s)\vee \exists X(r(s,X)\wedge \varepsilon _{\sqcap _0}(\mathsf {af}(|\varphi |),X))$, the last rule in the proof is $\vee _1$ or $\vee _2$. For $\vee _1$, $M\models \varepsilon _0(|\varphi |,s)$ holds by IH, then $M\models \varepsilon _0(\mathsf {af}(|\varphi |),s)$ holds by its semantic definition. For $\vee _2$, $M\models \exists X(r(s,X)\wedge \varepsilon _{\sqcap _0}(\mathsf {af}(|\varphi |),X))$ holds by IH, thus there exists $S'$ s.t. $M\models r(s,[S'])$ and $M\models \varepsilon _{\sqcap _0}(\mathsf {af}(|\varphi |),[S'])$ holds. Then we get $S'=\mathsf {next}(s)$ and for each state $s'$ in $S'$, $M\models \varepsilon _0(\mathsf {af}(|\varphi |), s')$ holds. Now assume $M\mid \!\ne \varepsilon _0(\mathsf {af}(|\varphi |), s)$, then there exists a lr-path $\rho (s)(j,k)$ s.t. $\forall 0\le i<k$, $M\mid \!\ne \varepsilon _0(|\varphi |,\rho _i)$. For the path $\rho (s)(j,k)$,

  • if $j\ne 0$, then $\rho ^k_1$ is a lr-path, which is a counterexample of $M\models \varepsilon _0(\mathsf {af}(|\varphi |), \rho _1)$.

  • if $j=0$, then $\rho ^k_1\hat{~~}\rho _1$ is a lr-path, which is a counterexample of $M\models \varepsilon _0(\mathsf {af}(|\varphi |), \rho _1)$.

  Thus $M\models \varepsilon _0(\mathsf {af}(|\varphi |),s)$ holds by its semantic definition.

• Suppose that $\vdash ^{cf}_{\mathcal {R}}\varepsilon _1(\mathsf {ag}(|\varphi |),s, [s^j_i])$ has a proof. As $\varepsilon _1(\mathsf {ag}(|\varphi |),s,[s^j_i])\hookrightarrow mem(s,[s^j_i])\vee (\varepsilon _0(|\varphi |,s)\wedge \exists X(r(s,X)\wedge \varepsilon _{\sqcap _1}(\mathsf {ag}(|\varphi |),X,\mathsf {con}(s,[s^j_i]))))$, the last rule in the proof is $\vee _1$ or $\vee _2$. For $\vee _1$, $M\models mem(s,[s^j_i])$ holds by IH, thus $s^j_i\hat{~~}s$ is a lr-path and $M\models \varepsilon _1(\mathsf {ag}(|\varphi |),s, [s^j_i])$ holds by its semantic definition. For $\vee _2$, $M\models \varepsilon _0(|\varphi |,s)$ and $M\models \exists X(r(s,X)\wedge \varepsilon _{\sqcap _1}(\mathsf {ag}(|\varphi |),X,\mathsf {con}(s,[s]^j_i)))$ holds by IH. Thus there exists $S'$ s.t. $M\models r(s,[S']) \wedge \varepsilon _{\sqcap _1}(\mathsf {ag}(|\varphi |),[S'],\mathsf {con}(s,[s^j_i]))$ holds. Then by the semantic definition, $S'=\mathsf {next}(s)$ and for each state $s'\in S'$, $M\models \varepsilon _1(\mathsf {ag}(|\varphi |),s',\mathsf {con}(s,[s^j_i]))$ holds. Thus $M\models \varepsilon _1(\mathsf {ag}(|\varphi |),s, [s^j_i])$ holds by its semantic definition.

Lemma 6

(Completeness). For a CTL formula $\varphi$ of NNF, if $M\models \varepsilon _0(|\varphi |,s)$, then the sequent $\vdash ^{cf}_{\mathcal {R}}\varepsilon _0(|\varphi |,s)$ has a proof.

Proof

By induction on the structure of $\varphi$. For brevity, here we just prove some of the cases. The full proof is in [10].

• Suppose $M\models \varepsilon _0(\mathsf {af}(|\varphi _1|),s)$ holds. By the semantics of $\mathcal {L}$, there exists a state $s'$ on each lr-path starting from s s.t. $M\models \varepsilon _0(|\varphi _1|,s')$ holds. Thus there exists a finite tree T s.t.

  • T has root s;

  • for each internal node $s'$ in T, the children of $s'$ are labelled by the elements of $\mathsf {next}(s')$;

  • for each leaf $s'$, $s'$ is the first node in the branch starting from s s.t. $M\models \varepsilon _0(|\varphi _1|,s')$ holds.

  By IH, for each leaf $s'$, there exists a proof $\varPi _{(\varphi _1,s')}$ for the sequent $\vdash ^{cf}_{\mathcal {R}}\varepsilon _0(|\varphi _1|,s')$. Then, to each subtree $T'$ of T, we associate a proof $|T'|$ of the sequent $\vdash ^{cf}_{\mathcal {R}}\varepsilon _0(\mathsf {af}(|\varphi _1|),s')$ where $s'$ is the root of $T'$, by induction, as follows,

  • if $T'$ contains a single node $s'$, then the proof $|T'|$ is as follows:

    

  • if $T'=s'(T_1,\ldots ,T_n)$, then the proof $|T'|$ is as follows:

    

  This way, |T| is a proof of the sequent $\vdash ^{cf}_{\mathcal {R}}\varepsilon _0(\mathsf {af}(|\varphi _1|),s)$.

• Suppose $M\models \varepsilon _0(\mathsf {ag}(|\varphi _1|),s)$ holds. By the semantics of $\mathcal {L}$, for each state $s'$ on each lr-path starting from s, $M\models \varepsilon _0(|\varphi _1|,s')$ holds. Thus there exists a finite tree T s.t.

  • T has root s;

  • for each internal node $s'$ in T, the children of $s'$ are labelled by the elements of $\mathsf {next}(s')$;

  • the branch starting from s to each leaf is a lr-path;

  • for each internal node $s'$ in T, $M\models \varepsilon _0(|\varphi _1|,s')$ holds and by IH, there exists a proof $\varPi _{(\varphi _1,s')}$ for the sequent $\vdash ^{cf}_{\mathcal {R}}\varepsilon _0(|\varphi _1|,s')$.

  Then, to each subtree $T'$ of T, we associate a proof $|T'|$ of the sequent $\vdash ^{cf}_{\mathcal {R}}\varepsilon _1(\mathsf {ag}(|\varphi _1|),s',[s'^{k-1}_0])$ where $s'$ is the root of $T'$ and $s'^k_0(s'_k=s')$ is the branch from s to $s'$, by induction, as follows,

  • if $T'$ contains a single node $s'$, then $s'^k_0$ is a lr-path and the proof is as follows:

    

  • if $T'=s'(T_1,\ldots ,T_n)$, the proof is as follows:

    

  This way, as $\varepsilon _0(\mathsf {ag}(|\varphi _1|),s)$ can be rewritten into $\varepsilon _1(\mathsf {ag}(|\varphi _1|),s,\mathsf {nil})$, |T| is a proof for the sequent $\vdash ^{cf}_{\mathcal {R}}\varepsilon _0(\mathsf {ag}(|\varphi _1|),s)$.    $\square$

Theorem 2

(Soundness and Completeness). For a CTL proposition $\varphi$ of NNF, the sequent $\vdash ^{cf}_{\mathcal {R}} \varepsilon _0(|\varphi |,s)$ has a proof iff $M\models \varepsilon _0(|\varphi |,s)$ holds.

6 Applications

6.1 Polarized Resolution Modulo

In Polarized Resolution Modulo, the polarized rewrite rules are taken as one-way clauses [6]. For example, the rewrite rule

$$\begin{aligned} \varepsilon _1(\mathsf {eg}(\varPhi ),x,Y) \hookrightarrow _+ mem(x,Y) \vee (\varepsilon _0(\varPhi ,x) \wedge \exists X(r(x,X) \wedge \varepsilon _{\sqcup _1}(\mathsf {eg}(\varPhi ),X,\mathsf {con}(x, Y)))) \end{aligned}$$

is translated into one-way clauses ${\underline{\varepsilon _1(\mathsf {eg}(\varPhi ),x,Y)}}\vee mem(x,Y)^{\bot }$ and ${\underline{\varepsilon _1(\mathsf {eg}(\varPhi ),x,Y)}} \vee \varepsilon _0(\varPhi ,x)^{\bot }\vee r(x,X)^{\bot }\vee \varepsilon _{\sqcup _1}(\mathsf {eg}(\varPhi ),X,\mathsf {con}(x,Y))^{\bot }$, in which the underlined literals have the priority to do resolution.

Fig. 4.

Resolution Example

Example 2

For the structure M in Fig. 4, we prove that $M,s_1\models _a EXEGp$. The one-way clauses of M are: ${\underline{\varepsilon _0(\mathsf {not}({\overline{p}}),s_1)}}$, ${\underline{\varepsilon _0({\overline{p}},s_2)}}$, ${\underline{\varepsilon _0({\overline{p}},s_3)}}$, ${\underline{r(s_1, \mathsf {con}(s_2,\mathsf {nil}))}}$, ${\underline{r(s_2, \mathsf {con}(s_3,\mathsf {nil}))}}$, ${\underline{r(s_3, \mathsf {con}(s_2,\mathsf {nil}))}}$. The translation of $M,s_1\models _a EXEGp$ is $\varepsilon _0(\mathsf {ex}(\mathsf {eg}({\overline{p}})),s_1)$ and the resolution steps start from

$\varepsilon _0(\mathsf {ex}(\mathsf {eg}({\overline{p}})),s_1)^{\bot }$.

First apply resolution with ${\underline{\varepsilon _0(\mathsf {ex}(\varPhi ),x)}}\vee r(x,X)^\bot \vee \varepsilon _{\sqcup _0}(\varPhi ,X)^\bot$, with $x=s_1$ and $\varPhi =\mathsf {eg}({\overline{p}})$, this yields

$r(s_1,X)^{\bot }\vee \varepsilon _{\sqcup _0}(\mathsf {eg}({\overline{p}}),X)^{\bot }$.

Then apply resolution with ${\underline{r(s_1, \mathsf {con}(s_2,\mathsf {nil}))}}$, with $X=\mathsf {con}(s_2,\mathsf {nil})$, this yields

$\varepsilon _{\sqcup _0}(\mathsf {eg}({\overline{p}}),\mathsf {con}(s_2,\mathsf {nil}))^{\bot }$.

Then apply resolution with ${\underline{\varepsilon _{\sqcup _0}(\varPhi ,\mathsf {con}(x,X))}}\vee \varepsilon _0(\varPhi ,x)^{\bot }$, with $x=s_2$, $X=\mathsf {nil}$ and $\varPhi =\mathsf {eg}({\overline{p}})$, this yields

$\varepsilon _0(\mathsf {eg}({\overline{p}}),s_2)^{\bot }$.

Then apply resolution with one-way clause ${\underline{\varepsilon _0(\mathsf {eg}(\varPhi ),x)}}\vee \varepsilon _1(\mathsf {eg}(\varPhi ),x,\mathsf {nil})^{\bot }$, with $\varPhi ={\overline{p}}$ and $x=s_2$, this yields

$\varepsilon _1(\mathsf {eg}({\overline{p}}),s_2,\mathsf {nil})^{\bot }$.

Then apply resolution with ($\ddagger$ ¹), with $\varPhi ={\overline{p}}$, $x=s_2$ and $Y=\mathsf {nil}$, this yields

$\varepsilon _0({\overline{p}},s_2)^{\bot }\vee r(s_2,X)^{\bot }\vee \varepsilon _{\sqcup _1}(\mathsf {eg}({\overline{p}}),X,\mathsf {con}(s_2,\mathsf {nil}))^{\bot }$.

Then apply resolution with ${\underline{\varepsilon _0({\overline{p}},s_2)}}$, this yields

$r(s_2,X)^{\bot }\vee \varepsilon _{\sqcup _1}(\mathsf {eg}({\overline{p}}),X,\mathsf {con}(s_2,\mathsf {nil}))^{\bot }$.

Then apply resolution with ${\underline{r(s_2, \mathsf {con}(s_3,\mathsf {nil}))}}$, with $X=\mathsf {con}(s_3,\mathsf {nil})$, this yields

$\varepsilon _{\sqcup _1}(\mathsf {eg}({\overline{p}}),\mathsf {con}(s_3,\mathsf {nil}),\mathsf {con}(s_2,\mathsf {nil}))^{\bot }$.

Then apply resolution with ${\underline{\varepsilon _{\sqcup _1}(\varPhi ,\mathsf {con}(x,X),Y)}}\vee \varepsilon _1(\varPhi ,x,Y)^{\bot }$, with $\varPhi =\mathsf {eg}({\overline{p}})$, $x=s_3$, $X=\mathsf {nil}$ and $Y=\mathsf {con}(s_2,\mathsf {nil})$, this yields

$\varepsilon _1(\mathsf {eg}({\overline{p}}),s_3,\mathsf {con}(s_2,\mathsf {nil}))^{\bot }$.

Then apply resolution with ($\ddagger$), with $\varPhi ={\overline{p}}$, $x=s_3$, $Y=\mathsf {con}(s_2,\mathsf {nil})$, this yields

$\varepsilon _0({\overline{p}},s_3)^{\bot }\vee r(s_3,X)^{\bot } \vee \varepsilon _{\sqcup _1}(\mathsf {eg}({\overline{p}}),X,\mathsf {con}(s_3,\mathsf {con}(s_2,\mathsf {nil})))^{\bot }$.

Then apply resolution with ${\underline{\varepsilon _0({\overline{p}},s_3)}}$, this yields

$r(s_3,X)^{\bot } \vee \varepsilon _{\sqcup _1}(\mathsf {eg}({\overline{p}}),X,\mathsf {con}(s_3,\mathsf {con}(s_2,\mathsf {nil})))^{\bot }$.

Then apply resolution with ${\underline{r(s_3, \mathsf {con}(s_2,\mathsf {nil}))}}$, with $X=\mathsf {con}(s_2,\mathsf {nil})$, this yields

$\varepsilon _{\sqcup _1}(\mathsf {eg}({\overline{p}}),\mathsf {con}(s_2,\mathsf {nil}),\mathsf {con}(s_3,\mathsf {con}(s_2,\mathsf {nil})))^{\bot }$.

Then apply resolution with ${\underline{\varepsilon _{\sqcup _1}(\varPhi ,\mathsf {con}(x,X),Y)}}\vee \varepsilon _1(\varPhi ,x,Y)^{\bot }$, with $\varPhi =\mathsf {eg}({\overline{p}})$, $x=s_3$, $X=\mathsf {nil}$ and $Y=\mathsf {con}(s_2,\mathsf {nil})$, this yields

$\varepsilon _1(\mathsf {eg}({\overline{p}}),s_2,\mathsf {con}(s_3,\mathsf {con}(s_2,\mathsf {nil})))^{\bot }$.

Then apply resolution with ${\underline{\varepsilon _1(\mathsf {eg}(\varPhi ),x,Y)}}\vee mem(x,Y)^{\bot }$, with $x=s_2$ and $Y=\mathsf {con}(s_3,\mathsf {con}(s_2,\mathsf {nil}))$, this yields

$mem(s_2,\mathsf {con}(s_3,\mathsf {con}(s_2,\mathsf {nil})))^{\bot }$.

Then apply resolution with ${\underline{mem(x,\mathsf {con}(y,Z))}}\vee mem(x,Z)^{\bot }$, with $x=s_2$, $y=s_3$ and $Z=\mathsf {con}(s_2,\mathsf {nil})$, this yields

$mem(s_2,\mathsf {con}(s_2,\mathsf {nil}))^{\bot }$.

Then apply resolution with ${\underline{mem(x,\mathsf {con}(x,Z))}}$, with $x=s_2$ and $Z=\mathsf {nil}$, this yields the empty clause. Thus $M,s_1\models _a EXEGp$ holds.

6.2 Experimental Evaluation

In this Section, we give a comparison between Resolution-based and QBF-based verification, that are implemented in iProver Modulo and VERDS [15] respectively. iProver Modulo is a prover by embedding Polarized Resolution Modulo into iProver [11]. The comparison is by proving 24 CTL properties on two kinds of programs: Programs with Concurrent Processes and Programs with Concurrent Sequential Processes. The programs and CTL properties refer to [16].

Table 1. Experimental Results

Table 2. Speed Comparisons

For the Con. Processes, each testing case contains 12/24 variables and 3 processes. For the Con. Seq. Processes, each testing case contains 12/16 variables and 2 processes. All the cases are tested on $\text {Intel}^{\circledR }$ $\text {Core}^{\text { TM}}$ i5-2400 CPU @ 3.10 GHz $\times$ 4 with Linux and the testing time of each case is limited to 20 min. The experimental data is presented in Tables 1 and 2 ². The comparison is based on two aspects: the number of testing cases that can be proved, and the time used if a problem can be proved in both. As can be seen in Table 1, among the 960 testing cases of the Con. Processes, 94 of them are timeout in iProver Modulo, while the number in VERDS is 99. For the Con. Seq. Processes, among the 960 testing cases, 173 of them are timeout in iProver Modulo, while in VERDS, the number is 260. Table 2 shows that, among the 818 testing cases of the Con. Processes, that are both proved in iProver Modulo and VERDS, iProver Modulo performs better in 272 of them and among the 678 testing cases of the Con. Seq. Processes, 412 of them run faster in iProver Modulo.

In summary, for the 1920 testing cases, 1653 ($86\,\%$) of them are solved by iProver Modulo, while 1561 ($81\,\%$) are solved by VERDS. For all the 1496 testing cases that are both proved, 684 ($45.8\,\%$) testing cases run faster in iProver Modulo.

7 Conclusion and Future Work

In this paper, we defined an alternative semantics for CTL, which is bounded to lr-paths. Based on the alternative semantics, a way to embed model checking problems into Deduction Modulo has been presented. Thus this work has given a method to solve model checking problems in automated theorem provers. An experimental evaluation of this approach using resolution modulo has been presented. The comparison with the QBF-based verification showed that automated theorem proving modulo, which performed as well as QBF-based method, can be considered as a new way to quickly determine whether a property is violated in transition system models.

The proof-search method does not work well on proving some temporal propositions, such as the propositions start with AG. One of the reasons is during the search steps, it may visit the same state repeatedly. To design new rewrite rules for the encoding of temporal connectives or new elimination rules to avoid this problem remains as future work.