Ying Jiang

Jian Liu
email: liujian@ios.ac.cn

Gilles Dowek
email: gilles.dowek@ens-cachan.fr

Kailiang Ji

Towards Combining Model Checking and Proof Checking

Keywords: CTL Model checking, Automated theorem proving, Continuation-passing style, Doubly on-the-fly style

Model checking and automated theorem proving are two pillars of formal verification methods. This paper investigates model checking from an automated theorem proving perspective, aiming at combining the expressiveness of automated theorem proving and the complete automaticity of model checking. It places the focus on the verification of temporal logic properties of Kripke models. The main contributions are: (1) introducing an extended computation tree logic that allows polyadic predicate symbols; (2) designing a proof system for this logic, taking Kripke models as parameters;

(3) developing a proof search algorithm for this system and a new automated theorem prover to implement it. The verification process of the new prover is completely automatic, and produces either a counterexample when the property does not hold, or a certificate when it does. The experimental results compare well to existing state-of-the-art tools on some benchmarks, and the efficiency is illustrated by application to an air traffic control problem.

INTRODUCTION

Model checking [START_REF] Clarke | Model checking[END_REF][START_REF] Bouajjani | Regular model checking[END_REF][START_REF] Baier | Principles of Model Checking[END_REF] and automated theorem proving [START_REF] Fitting | First-Order Logic and Automated Theorem Proving[END_REF][START_REF] Loveland | Automated Theorem Proving: A Logical Basis[END_REF][START_REF] Burel | Automating theories in intuitionistic logic[END_REF] are two pillars of formal verification methods. They differ by the fact that model checking often uses decidable logics, such as propositional modal logics, while automated theorem proving mostly uses undecidable ones, such as firstorder logic. Nevertheless, model checking and automated theorem proving have a lot in common, in particular, both of them are often based on a recursive decomposition of problems, through the application of rules.

This paper investigates model checking from an automated theorem proving perspective, aiming at combining the expressiveness of automated theorem proving and the complete automaticity of model checking.

The first contribution of this paper is to propose a slight extension of Computation Tree Logic (CTL) [START_REF] Emerson | Using branching time temporal logic to synthesize synchronization skeletons[END_REF][START_REF] Emerson | Decision procedures and expressiveness in the temporal logic of branching time[END_REF], called CTL P . In this extension, we may refer explicitly to states of the model under consideration. For instance, the proposition P(s) expresses what is usually expressed with the judgment s |= P. Thus P here is not a proposition symbol, but a unary predicate symbol. This transformation can be compared to the introduction of adverbial phrases in natural languages, where we can say not only "The sky will be blue in the future" but also "The sky will be blue on Monday". A proposition such as EX(P)(s) must then be written as EX x (P(x))(s). Indeed, as the symbol P is now a unary predicate symbol, it must be applied to a variable, which is bound by the modality EX. This allows to introduce polyadic predicates that do not only express properties of states, but also relations between states. For instance, we can express the existence of a sequence of states s 0 , s 1 , ... such that each s i+1 occurs after s i and that one can buy a left shoe at some state s m and then the right shoe of the same pair at a later state s n . This property is expressed by the formula EF x (EF y (P(x, y))(x))(s 0 ) in CTL P .

The second contribution of this paper is to propose a sequent-calculus-like proof system for CTL P , called simply SCTL. The proof search in SCTL coincides with checking the validity of properties described by CTL P formulae in a Kripke model. We prove that SCTL is sound and complete and the proof search in this system always terminates.

When designing such a proof system, one of the main issues is to handle co-inductive modalities, for instance, asserting the existence of an infinite sequence of which all elements satisfy some property. It is tempting to reflect this infinite sequence as an infinite proof and then use the finiteness of the model to prune the search-tree in a proof search method. Instead, we use the finiteness of the model to keep our proofs finite, like in the usual sequent calculus. This is the purpose of the merge rules of SCTL (Figure 4). However, the way we use sequents in SCTL is a bit unusual: as we prove a sequent of the form A ⇒ B by proving B or by proving ¬A, and not by proving A B, we do not need hypotheses to prove implications. So we use the left hand side of the sequent to store visited states for co-inductive modalities.

SCTL enjoys several advantages. For example, when a given property holds in a Kripke model, it permits to give a certificate (a proof tree) for the property. Such a certificate can be further verified by an independent proof checker, increasing the confidence in the proved property, and can also be combined with proofs built by other means. Conversely, when a given property does not hold, it permits to generate a counterexample as a proof of the negation of the property, instead of a sequence of states as in traditional model checkers. In particular, when providing a counterexample for a formula containing nested modalities, such as EG x (EG y (P(x, y))(x))(s), we need to provide a finite tree labeled with states, in such a way that for each state a labeling a leaf of this tree, the formula EG y (P(a, y))(a)) does not hold. Thus, for each of these states, we need to provide another tree. As we shall see, such a hierarchical tree can be represented as a proof of the formula AF x (AF y (¬P(x, y))(x))(s) in SCTL.

The third contribution of this paper is an implementation of SCTL. Instead of translating temporal formulae to Quantified Boolean Formulae (QBFs) [START_REF] Zhang | QBF encoding of temporal properties and QBF-based verification[END_REF] or to the format of an existing theorem prover [START_REF] Ji | CTL model checking in deduction modulo[END_REF], we develop a new automated theorem prover tailored for SCTL (SCTLProV 5 ), in the programming language OCaml. 6Designing our own system permits us to combine the advantages of model checking and automated theorem proving, and gives us a lot of freedom to optimize it. For example, SCTLProV adopts several techniques, such as global variable storage or storage based on Binary Decision Diagram (BDD), which are commonly used in traditional model checkers, but cannot be realized in the usual theorem provers like iProver Modulo. On the other hand, theorem provers usually output proof trees as a diagnosis of the system under verification, while in traditional model checkers, only sequences of states representing the counterexamples can be produced. One inheritance from traditional theorem provers is that SCTLProV produces proof trees in any case. Another inheritance is that, in SCTLProV, the Kripke model is not always defined extensionally with a list of states and a list of transitions, but the type of states can be any datatype and the transitions can be defined by an arbitrary computable function mapping a state to the list of its successors. Therefore SCTLProV provides a more expressive input language than most traditional model checkers. This choice allows us to tackle, for instance, the Small Aircraft Transportation System (SATS) [START_REF] Muñoz | Modeling and verification of an air traffic concept of operations[END_REF][START_REF]Abstract Model of SATS Concept of Operations: Initial Results and Recommendations[END_REF], that is often difficult to solve for model checkers using a more extensional description of their input.

To illustrate the efficiency of SCTLProV, we compared the experimental data of SCTLProV, on several benchmarks, with the following tools: an automated theorem prover iProver Modulo7 , a QBF-based bounded model checker Verds8 , two BDD-based symbolic model checkers NuSMV9 and NuXMV10 , and the verification toolbox CADP 11 for action based models. The experimental results show that SCTLProV compares well with these tools.

The reason for selecting the tools above-mentioned is: firstly, the focus of this work is on solving CTL model checking problems while, as far as we know, NuSMV and NuXMV are the most successful model checkers up-todate in this area; secondly, benchmark #1 in this paper is originally proposed by Zhang [START_REF] Zhang | QBF encoding of temporal properties and QBF-based verification[END_REF] in order to compare the bounded model checker Verds with NuSMV, and reused by Ji [START_REF] Ji | CTL model checking in deduction modulo[END_REF] to compare the theorem prover iProver Modulo with Verds; finally, as one of the state-of-the-art explicit model checkers, CADP is widely used both in industrial and academic fields.

The efficiency of SCTLProV depends on the following design choices: the first is that, unlike traditional symbolic model checkers or bounded model checkers, SCTLProV searches states in a doubly on-the-fly style (both the transition relation and the formula are unfolded on-the-fly) [START_REF] Bhat | Efficient on-the-fly model checking for ctl *[END_REF][START_REF] Vergauwen | A linear local model checking algorithm for CTL[END_REF]. Thus, the state space is usually not needed to be fully generated. This avoids enumerating unneeded states during the verification procedure. The second is that, unlike traditional on-the-fly model checking algorithms for CTL [START_REF] Bhat | Efficient on-the-fly model checking for ctl *[END_REF][START_REF] Vergauwen | A linear local model checking algorithm for CTL[END_REF], our proof search algorithm is in continuationpassing style [START_REF] Appel | Compiling with Continuations (corr. version)[END_REF] which permits to reduce stack operations.

Links between model checking and automated theorem proving have been investigated for long, for instance, Bounded Model Checking (BMC) [START_REF] Biere | Symbolic model checking without BDDs[END_REF][START_REF] Zhang | QBF encoding of temporal properties and QBF-based verification[END_REF][START_REF] Biere | Bounded model checking[END_REF] is based on a reduction of model checking to satisfiability of Boolean or quantified Boolean formulae. In the literature, different proof systems for temporal logic have been proposed [START_REF] Emerson | Decision procedures and expressiveness in the temporal logic of branching time[END_REF][START_REF] Fisher | Clausal temporal resolution[END_REF][START_REF] Gabbay | A sound and complete deductive system for ctl* verification[END_REF][START_REF] Pnueli | A deductive proof system for CTL[END_REF][START_REF] Reynolds | An axiomatization of full computation tree logic[END_REF][START_REF] Brünnler | Cut-free sequent systems for temporal logic[END_REF]. Proof systems for temporal logics usually deal with the validity problem [START_REF] Emerson | Decision procedures and expressiveness in the temporal logic of branching time[END_REF][START_REF] Fisher | Clausal temporal resolution[END_REF][START_REF] Brünnler | Cut-free sequent systems for temporal logic[END_REF], where a temporal formula is provable if and only if it holds in all models. However, the proof system SCTL is parameterized by Kripke models, in the sense that, for any given Kripke model M , a CTL P formula is provable in SCTL if and only if it holds in M . The rest of the paper is organized as follows. In Section 2, we introduce the logic CTL P . In Section 3, we introduce the proof system SCTL. In Section 4, first we present the proof search algorithm for SCTL and the complete automatic prover SCTLProV which is an implementation of SCTL; then the design choices of SCTLProV will be discussed in more detail. In Section 5, we deal with the verification of properties under fairness constraints in SCTL. In Section 6, first we compare, on several benchmarks, SCTLProV with iProver Modulo, Verds, NuSMV, NuXMV, and CADP, respectively; then we illustrate the application of SCTLProV by modeling and analyzing SATS and verifying its safety property. Appendix A describes in detail the pseudo code of the proof search algorithm. Appendix B shows the details of the experimental data for benchmark #1, #2, #3, and #4. Appendix C shows the detailed proofs for the soundness and completeness of the proof system SCTL. Appendix D shows the detailed proof for the correctness of the proof search method.

CTL P

In this section, we present the logic CTL P (M ) taking a Kripke model M as the parameter. • a finite non-empty set S, whose elements are called states,

• a binary relation -→ defined on S, such that for each s in S, there exists a finite number of elements and at least one element s in S, such that s -→ s ,

• and a family of relations, each being a subset of S n for some natural number n.

We write Next(s) for the set {s ∈ S | s -→ s } which is always finite and not empty. A path is a finite or infinite sequence of states s 0 , ..., s n or s 0 , s 1 , ... such that for each i, if s i is not the last element of the sequence, then s i+1 ∈ Next(s i ). A path-tree is a finite or infinite tree labeled by states such that for each internal node labeled by a state s, the children of this node are labeled by exactly the elements of Next(s).

Properties of such a model are expressed in a language tailored for this model that contains a constant for each state s, also written as s; and a predicate symbol for each relation P, also written as P.

The grammar of CTL P (M ) formulae is displayed below:

φ :=    | ⊥ | P(t 1 , ...,t n ) |¬P(t 1 , ...,t n ) | φ ∧ φ | φ ∨ φ | AX x (φ)(t) | EX x (φ)(t) | AF x (φ)(t) | EG x (φ)(t) | AR x,y (φ 1 , φ 2 )(t) | EU x,y (φ 1 , φ 2 )(t)
where x, y are variables, and each of t and t 1 . . .t n is either a constant or a variable.

Note that in this language, modalities are applied to formulae and states, binding variables in these formulae. More explicitly, modalities AX, EX, AF, and EG bind the variable x in φ, and modalities AR and EU bind respectively the variable x in φ 1 and y in φ 2 . Also, the negation is applied to atomic formulae only, so, as usual, negations must be pushed inside the formulae. We use the notation (t/x)φ for the substitution of t for all free occurrences of x in φ. As usual, in presence of binders, substitution avoids variable captures.

The following abbreviations are used.

• φ 1 ⇒ φ 2 ≡ ¬φ 1 ∨ φ 2 ; • EF x (φ)(t) ≡ EU z,x ( , φ)(t); • ER x,y (φ 1 , φ 2 )(t) ≡ EU y,z (φ 2 , ((z/x)φ 1 ∧ (z/y)φ 2 ))(t) ∨ EG y (φ 2 )(t)
, where z is a variable that occurs neither in φ 1 nor in φ 2 ;

• AG x (φ)(t) ≡ ¬(EF x (¬φ)(t)); • AU x,y (φ 1 , φ 2 )(t) ≡ ¬(ER x,y (¬φ 1 , ¬φ 2 )(t)).
Hereafter, each of AX, EX, AF, EF, AU, and EU is called an inductive modality; and each of AR, ER, AG, and EG is called a co-inductive modality. A formula starting with an inductive modality is called an inductive formula; and a formula starting with a co-inductive modality is called a coinductive formula. DEFINITION 2.2 (Validity). Let M be a Kripke model and φ be a closed CTL P formula. The validity of the formula φ in the model M is defined by induction on φ in Figure 1.

From this definition, we obtain M |= EF x (φ)(s), if there exists an infinite path s 0 , s 1 , ... starting from s and a natural number j such that M |= (s j /x)φ, etc. EXAMPLE 1. The formula

EF x (EF y (P(x, y))(x))(a)
expresses the existence of a path starting from state a, that contains two states related by P. This formula is valid in a Kripke model formed with the relation depicted below

a b c d e
and the set P = { a, c }, but not in that formed with the same relation and the set P = { a, d } instead. EXAMPLE 2. This example is inspired from the example presented in [START_REF] Partovi | Assume-guarantee cooperative satisfaction of multi-agent systems[END_REF], where the specification of the motion planning of a multi-robot [START_REF] Craig | Introduction to Robotics -Mechanics and Control[END_REF] system is characterized by CTL formulae. The specification states that, on a partitioned map, each robot moving from an initial section will eventually reach its destination section; meanwhile, along the movement, each robot should avoid entering some specific section. Here we focus on "spatial" properties (i.e., properties that characterize relations between states). Consider a special robot, e.g. an unmanned vehicle, that is designed to move on the surface of a planet. The planet is partitioned into a finite number of small areas. The unmanned vehicle moves from one area to another at a time, each position of the unmanned vehicle is considered as a state, and the moves from one position to another form the transition relation. A basic property of which a unmanned vehicle designer has to think is that: a unmanned vehicle should not stay infinitely long in a small set of areas. To be more precise, for a given distance σ, at any state s, the unmanned vehicle will eventually move to some state s such that the distance (not the number of moves) between s and s is longer than σ. This property can be easily characterized by the CTL P formula AG x (AF y (D σ (x, y))(x))(s 0 ), where s 0 is the landing position of the unmanned vehicle, i.e., the initial state; and atomic formula D σ (x, y) characterizes the spatial property that the distance between state x and state y is longer than σ. This scenario is depicted in Figure 2. This kind of properties can be easily expressed in CTL P , but cannot be elegantly, even impossibly, expressed in CTL, as there are no mechanisms to speak about specific states in THE COMPUTER JOURNAL, Vol. ??, No. ??, ????

SCTL

In this section, we present SCTL(M ), a proof system for CTL P (M ) taking a Kripke model as the parameter. 12 Unlike the usual proof systems, where a formula is provable if and only if it is valid in all models, a formula is provable in SCTL(M ) if and only if it is valid in the Kripke model M .

Proofs

Consider the formula AF x (P(x))(s). This formula is valid if there exists a finite path-tree whose root is labeled by s, and all the leaves are in P. Such a tree can be called a proof of the formula AF x (P(x))(s).

Consider now the formula AF x (AF y (P(x, y))(x))(s) that contains nested modalities. To justify the validity of this formula, one needs to provide a path-tree whose root is labeled by s, and at each leaf a, the formula AF y (P(a, y))(a) is valid. To justify the validity of the formula AF y (P(a, y))(a), one needs to provide other pathtrees. These hierarchical trees can be formalized with the following proof rules.

(s/x)φ AF x (φ)(s) AF-R 1 AF x (φ)(s 1 ) . . . AF x (φ)(s n ) AF x (φ)(s) AF-R 2
P(b) atom-R AF x (P(x))(b) AF-R 1 P(c) atom-R AF x (P(x))(c) AF-R 1 AF x (P(x))(a) AF-R 2
where besides the rules AF-R 1 and AF-R 2 , we use the following rule.

P(s 1 , ..., s n ) atom-R
= { b, d , c, d }. A proof of the formula AF x (AF y (Q(x, y))(x))(a) is given in Figure 3.
In the usual sequent calculus, the right rule of disjunction can either be formulated in a multiplicative way

Γ φ 1 , φ 2 , ∆ Γ φ 1 ∨ φ 2 , ∆
or in an additive way

Γ φ 1 , ∆ Γ φ 1 ∨ φ 2 , ∆ AF-R 2 FIGURE 3. A proof of AF x (AF y (Q(x, y))(x))(a) Γ φ 2 , ∆ Γ φ 1 ∨ φ 2 , ∆
These two formulations are equivalent in presence of structural rules. For instance, the proof of the sequent P ⇒ P, that is ¬P ∨ P, in the multiplicative system The contraction rule, or the multiplicative rule, is needed to build the sequent ¬P, P that is provable even if none of its weakenings ¬P and P is, because we do not know whether the formula P is true or false.

Our proof system SCTL needs neither contraction rules nor multiplicative ∨-R rules, because for each atomic formula P, either P is provable or ¬P is. Therefore, the sequent ¬P ∨ P is proved by proving either the sequent ¬P or the sequent P.

As we have neither multiplicative ∨-R rules nor structural rules, if we start with a sequent φ, where the formula φ does not contain co-inductive sub-formulae, then each sequent in the proof has one formula on the right of and none on the left. Thus, as all sequents have the form φ, the left rules and the axiom rule can be dropped as well. In other words, unlike the usual sequent calculus, our proof system, like Hilbert systems, is tailored for deduction, not for hypothetical deduction.

The case of co-inductive formulae, for instance EG x (P(x))(s), is more complex than that of the inductive formulae. To justify its validity, one needs to provide an infinite sequence that is an infinite path-tree with only one branch, such that the root of the tree is labeled by s, and each state in the infinite sequence verifies P. As the model is finite, we can always restrict to regular trees and use a finite representation of such trees. This leads us to introduce a rule, called EG-merge, that permits to prove a sequent of the form EG x (P(x))(s), provided such a sequent already occurs lower in the proof. To make this rule local, we re-introduce hypotheses Γ to record part of the history of the proof. 13 The sequents have therefore the form Γ φ, with a non-empty Γ in this particular case only, and the EG-merge rule is then just an instance of the axiom rule.

The above discussion leads to the rules of SCTL depicted in Figure 4.

Soundness and completeness

Proposition 3.1 and 3.2 below permit to transform finite structures into infinite ones and will be used in the Soundness proof, while Proposition 3.3 and 3.4 permit to transform infinite structures into finite ones and will be used in the Completeness proof. PROPOSITION 3.1 (Finite to infinite sequences). Let s 0 , ..., s n be a finite sequence of states such that for all i between 0 and n -1, s i -→ s i+1 , and s n = s p for some p between 0 and n -1. Then there exists an infinite sequence of states s 0 , s 1 , ... such that s 0 = s 0 and for all i, s i -→ s i+1 , and all the s j are among s 0 , ..., s n .

Proof. Take the sequence s 0 , ..., s p-1 , s p , ..., s n-1 , s p , ..., where s 0 = s 0 . PROPOSITION 3.2 (Finite to possibly infinite path-trees). Let S be a set of states and T be a finite path-tree such that each leaf is labeled with a state which is either in S or also a label of a node on the branch from the root of T to this leaf. Then, there exists a possibly infinite path-tree T such that all the leaves are labeled by elements of S, and all the labels of T are the labels of T .

Proof. Consider for T the path-tree whose root is labeled by the root of T and such that for each node s, if s is in S, then s is a leaf of T , otherwise the successors of s are the elements of Next(s). It is easy to check that all the nodes of T are labeled by labels of T . PROPOSITION 3.3 (Infinite to finite sequences). Let s 0 , s 1 , ... be an infinite sequence of states such that for all i, s i -→ s i+1 . Then there exists a finite sequence of states s 0 , ..., s n such that for all i between 0 and n -1, s i -→ s i+1 , s n = s p for some p between 0 and n -1, and all the s j are among s 0 , s 1 , ... Proof. As the number of states is finite, there exists p and n such that p < n and s p = s n . Take the sequence s 0 , ..., s n .

P(s 1 , ..., s n ) atom-R s 1 ,...,s n ∈P ¬P(s 1 , ..., s n ) ¬-R s 1 ,...,s n / ∈P -R φ 1 φ 2 φ 1 ∧ φ 2 ∧-R φ 1 φ 1 ∨ φ 2 ∨-R 1 φ 2 φ 1 ∨ φ 2 ∨-R 2 (s /x)φ EX x (φ)(s) EX-R s ∈Next(s) (s 1 /x)φ . . . (s n /x)φ AX x (φ)(s) AX-R {s 1 ,...,s n }=Next(s) (s/x)φ AF x (φ)(s) AF-R 1 AF x (φ)(s 1 ) . . . AF x (φ)(s n ) AF x (φ)(s) AF-R 2 {s 1 ,...,s n }=Next(s) (s/x)φ Γ EG x (φ)(s ) Γ EG x (φ)(s) EG-R s ∈Next(s); Γ =Γ,EG x (φ)(s) Γ EG x (φ)(s) EG-merge EG x (φ)(s)∈Γ (s/y)φ 2 Γ AR x,y (φ 1 , φ 2 )(s 1 ) ... Γ AR x,y (φ 1 , φ 2 )(s n ) Γ AR x,y (φ 1 , φ 2 )(s) AR-R 1 {s 1 ,...,s n }=Next(s); Γ =Γ,AR x,y (φ 1 ,φ 2 )(s) (s/x)φ 1 (s/y)φ 2 Γ AR x,y (φ 1 , φ 2 )(s) AR-R 2 Γ AR x,y (φ 1 , φ 2 )(s) AR-merge AR x,y (φ 1 ,φ 2 )(s)∈Γ (s/y)φ 2 EU x,y (φ 1 , φ 2 )(s) EU-R 1 (s/x)φ 1 EU x,y (φ 1 , φ 2 )(s ) EU x,y (φ 1 , φ 2 )(s) EU-R 2 s ∈Next(s) FIGURE 4. SCTL(M )
PROPOSITION 3.4 (Possibly infinite to finite path-trees). Let S be a set of states and T be a possibly infinite path-tree such that each leaf is labeled by a state in S. Then, there exists a finite path-tree such that each leaf is labeled with a state which is either in S or also a label of a node on the branch from the root of T to this leaf.

Proof. As the number of states is finite, on each infinite branch, there exists p and n such that p < n and s p = s n . Prune the path-tree at node s n . This path-tree is finitely branching and each branch is finite, hence, by König's lemma, it is finite.

IMPLEMENTATION

In this section, a proof search method for SCTL is presented. Based on this method, a proof search algorithm is designed. Based on this algorithm, a complete automatic prover SCTLProV 14 is developed, verifying CTL P properties over 14 https://github.com/sctlprov/sctlprov_code any Kripke models. Finally, we discuss the relations of the techniques adopted in SCTLProV with those in some other CTL model checking approaches.

A proof search method for SCTL

The basic idea of the proof search method for SCTL is as follows: firstly, an order is given over the inference rules of SCTL with the same conclusion; secondly, for each inference rule, an order is given over its premises. This way, proving the sequent transforms into proving all its premises with some specific order. The purpose of continuationpassing tree (Definition 4.1) is to encode these two orders into a tree-like structure when proving a sequent. This proof search method leads to the CPT rewriting system displayed in Figure 5.

Continuations and CPT rewriting system

The major technique for the proof search method is based on the concept of continuation, which is usually used in compiling and programming [START_REF] Appel | Compiling with Continuations (corr. version)[END_REF][START_REF] Sestoft | Programming Language Concepts[END_REF]. Basically, a continuation is an explicit representation of "the rest of the computation" to happen. • every internal node is labeled by an SCTL sequent.

), c 1 , c 2 ) c 1 [ s 1 , ..., s n / ∈ P] cpt( φ 1 ∧ φ 2 , c 1 , c 2 ) cpt( φ 1 , cpt( φ 2 , c 1 , c 2 ), c 2 ) cpt( φ 1 ∨ φ 2 , c 1 , c 2 ) cpt( φ 1 , c 1 , cpt( φ 2 , c 1 , c 2 )) cpt( AX x (φ)(s), c 1 , c 2 ) cpt( (s 1 /x)φ, cpt( (s 2 /x)φ, cpt(...cpt( (s n /x)φ, c 1 , c 2 ), ..., c 2 ), c 2 ), c 2 ) [{s 1 , ..., s n } = Next(s)] cpt( EX x (φ)(s), c 1 , c 2 ) cpt( (s 1 /x)φ, c 1 , cpt( (s 2 /x)φ, c 1 , cpt(...cpt( (s n /x)φ, c 1 , c 2 )...))) [{s 1 , ..., s n } = Next(s)] cpt(Γ AF x (φ)(s), c 1 , c 2 ) c 2 [AF x (φ)(s) ∈ Γ] cpt(Γ AF x (φ)(s), c 1 , c 2 ) cpt( (s/x)φ, c 1 , cpt(Γ AF x (φ)(s 1 ), cpt(...cpt(Γ AF x (φ)(s n ), c 1 , c 2 )..., c 2 ), c 2 )) [{s 1 , ..., s n } = Next(s), AF x (φ)(s) / ∈ Γ, and Γ = Γ, AF x (φ)(s)] cpt(Γ EG x (φ)(s), c 1 , c 2 ) c 1 [EG x (φ)(s) ∈ Γ] cpt(Γ EG x (φ)(s), c 1 , c 2 ) cpt( (s/x)φ, cpt(Γ EG x (φ)(s 1 ), c 1 , cpt(...cpt(Γ EG x (φ)(s n ), c 1 , c 2 )...)), c 2 ) [{s 1 , ..., s n } = Next(s), EG x (φ)(s) / ∈ Γ, and Γ = Γ, EG x (φ)(s)] cpt(Γ AR x,y (φ 1 , φ 2 )(s), c 1 , c 2 ) c 1 (AR x,y (φ 1 , φ 2 )(s) ∈ Γ cpt(Γ AR x,y (φ 1 , φ 2 )(s), c 1 , c 2 ) cpt( (s/y)φ 2 , cpt( (s/x)φ 1 , c 1 , cpt(Γ AR x,y (φ 1 , φ 2 )(s 1 ), cpt(...cpt(Γ AR x,y (φ 1 , φ 2 )(s n ), c 1 , c 2 )..., c 2 ), c 2 )), c 2 ) {s 1 , ..., s n } = Next(s), AR x,y (φ 1 , φ 2 )(s) / ∈ Γ, and Γ = Γ, AR x,y (φ 1 , φ 2 )(s) cpt(Γ EU x,y (φ 1 , φ 2 )(s), c 1 , c 2 ) c 2 EU x,y (φ 1 , φ 2 )(s) ∈ Γ cpt(Γ EU x,y (φ 1 , φ 2 )(s), c 1 , c 2 ) cpt( (s/y)φ 2 , c 1 , cpt( (s/x)φ 1 , cpt(Γ EU x,y (φ 1 , φ 2 )(s 1 ), c 1 , cpt(...cpt(Γ EU x,y (φ 1 , φ 2 )(s n ), c 1 , c 2 )...)), c 2 ))
For each internal node in a CPT, the left sub-tree is called its t-continuation, and the right one its f-continuation. A CPT c with a SCTL sequent Γ φ labeled at its root is called a CPT corresponding to the sequent Γ φ, and often denoted by cpt(Γ φ, c 1 , c 2 ), or visually by

Γ φ c 1 c 2
where c 1 is the t-continuation of c, and c 2 the f-continuation.

The proof system SCTL is implemented by the CPT rewriting system given in Figure 5, where conditions are put in brackets. Since there is no congruence rule to allow the application of a rewrite rule to a sub-expression of a CPT, reductions always occur at the root of a CPT.

The aim of these conditional rewrite rules is to decide, for a given sequent Γ φ, whether the corresponding CPT, that is cpt(Γ φ, t, f), reduces to t or to f. To do so, we analyze the form of the formula φ. If, for instance, it is φ 1 ∧ φ 2 , we transform, using one of the rewrite rules, the tree cpt(

φ 1 ∧ φ 2 , t, f) into cpt( φ 1 , cpt( φ 2 , t, f), f) which is depicted as φ 1 φ 2 t f f
expressing that if the attempt to prove φ 1 succeeds, then we attempt to prove φ 2 , otherwise it just returns a negative result denoted by f. Then the reduction procedure will apply to cpt( φ 1 , cpt( φ 2 , t, f), f) by considering the form of φ 1 , and so on. EXAMPLE 5. The proof search method can be illustrated by searching the proof in Example 3. The rewriting steps are depicted in Figure 6.

Step 1. Consider the CPT on the left side of 1 , the root of it is labeled by AF x (P(x))(a) which is the sequent to prove. We need to decide whether AF x (P(x))(a) is provable, which is not known at that moment yet, so the leaves of the CPT are its t-continuation and f-continuation, representing the rest of the proof search. Then we have to decide successively THE COMPUTER JOURNAL, Vol. ??, No. ??, ????

AF x (P(x))(a) t f 1 P(a) t Γ 1 AF x (P(x))(b) Γ 1 AF x (P(x))(c) t f f 2 Γ 1 AF x (P(x))(b) Γ 1 AF x (P(x))(c) t f f 3 P(b) Γ 1 AF x (P(x))(c) t f Γ 2 AF x (P(x))(d) Γ 1 AF x (P(x))(c) t f f 4 Γ 1 AF x (P(x))(c) t f 5 P(c) t Γ 3 AF x (P(x))(d) t f 6 t where Γ 1 = {AF x (P(x))(a)}, Γ 2 = Γ 1 ∪ {AF x (P(x))(b)} and Γ 3 = Γ 1 ∪ {AF x (P(x))(c)} FIGURE 6. An illustration of CPT rewritings • If AF x (P(x))(a) is provable by applying the AF-R 1 rule, that is, if P(a) is provable. • If AF x (P(x))(a) is provable by applying the AF- R 2 rule, that is, if Γ 1 AF x (P(x))(b) and Γ 1 AF x (P(x))(c) are provable, successively.
The above information is encoded into a single CPT that is on the right side of 1 .

Step 2. Since the atomic formula P(a) is not provable, we can only use the AF-R 2 rule to prove AF x (P(x))(a), so the CPT on the left side of 2 reduces to its right sub-tree (f-continuation) which is the CPT on the right side of 2 .

Step 3. Like at step 1, we need to decide if Γ 1 AF x (P(x))(b) is provable, which is not known at that moment. According to the CPT which is on the left side of 3 , we know that if Γ 1 AF x (P(x))(b) is provable then we need to decide if Γ 1 AF x (P(x))(c) is provable. Then we have to decide successively

• If Γ 1 AF x (P(x))(b) is provable by applying the AF- R 1 rule, that is, if P(b) is provable. • If Γ 1 AF x (P(x))(b) is provable by applying the AF- R 2 rule, that is, if Γ 2 AF x (P(x))(d) is provable.
The above information is encoded into a single CPT that is on the right side of 3 .

Step 4. Like at step 2, we can judge that the atomic formula P(b) is provable immediately. So the CPT on the left side of 4 reduces to its left sub-tree (t-continuation) which is on the right side of 4 .

Step 5. Like at step 1 and 3, we can not judge whether the sequent Γ 1 AF x (P(x))(c) is provable immediately, so we encode the two steps to find successively the proofs of P(c) and Γ 3 AF x (P(x))(d) into the CPT which is on the right side of 5 ;

Step 6. Like at step 2 and 4, as the atomic formula P(c) is provable, the CPT on the left side of 6 reduces to its left sub-tree (t-continuation) which is t. Now, the proof search of AF x (P(x))(a) terminates, and we can judge that this sequent is provable.

It is worth to note that the proof system SCTL is sound and complete, but the proof search in SCTL does not always terminate : this is the case when the formula under consideration is an inductive formula and it is not provable. However, if we introduce merge rules for each inductive modalities as well, then proof search always terminates. More precisely, although we do not need merge rules for inductive formulae (formulae starting with modalities AF or EU etc.) in the proof system SCTL, we do need merge rules for this kind of formulae in the CPT rewriting system which provides a proof search method for SCTL. This is because, for instance, to search a proof of the sequent EU x,y (φ 1 , φ 2 )(s), we need to find a finite path of states, say s 0 (= s), . . . , s n , in the Kripke model M under consideration, such that φ 2 holds at state s n , and φ 1 holds at all other state s i (if any). However, M may also contain infinite paths of states, say s 0 (= s), s 1 , . . . such that φ 1 holds at each state s i (i ≥ 0), and φ 2 does not hold at any of them. On such an infinite path, the proof search procedure for the sequent EU x,y (φ 1 , φ 2 )(s) cannot terminate. To deal with this kind of scenarios, in the CPT rewriting system, the merge rules for inductive formulae are introduced.

Note also that merges for inductive and co-inductive formulae are different in the CPT rewriting system. Intuitively, in the case of co-inductive formulae: consider, for example, the sequent Γ EG x (φ)(s).

• If EG x (φ)(s) ∈ Γ, then we have cpt(Γ EG x (φ)(s), c 1 , c 2 )
c 1 according to the CPT rewriting system, and we proceed with the reduction of c 1 , where cpt

(Γ EG x (φ)(s), c 1 , c 2 ) is a corresponding CPT of the sequent Γ EG x (φ)(s). • If EG x (φ)(s) ∈ Γ,
then one of the following cases holds:

- if (s/x)φ is not provable in SCTL, then we have cpt(Γ EG x (φ)(s), c 1 , c 2 ) * c 2 ,
and proceed with the reduction of c 2 , where cpt(Γ THE COMPUTER JOURNAL, Vol. ??, No. ??, ????

EG x (φ)(s), c 1 , c 2 ) is a corresponding CPT of the sequent Γ EG x (φ)(s); - otherwise, EG x (φ)(s)
is added into the context, and we proceed with the reduction of a corresponding CPT of a sequent Γ EG x (φ)(s ), where Γ = Γ ∪ {EG x (φ)(s)} and s ∈ Next(s).

In the case of inductive formulae: consider, for example, the sequent Γ AF x (φ)(s).

• If AF x (φ)(s) ∈ Γ, then there exists a rewriting step cpt(Γ AF x (φ)(s), c 1 , c 2 )
c 2 according to the CPT rewriting system, and we proceed with the reduction of c 2 , where cpt

(Γ AF x (φ)(s), c 1 , c 2 ) is a corresponding CPT of the sequent Γ AF x (φ)(s). • If AF x (φ)(s) ∈ Γ,
then one of the following cases holds:

- if (s/x)φ is provable in SCTL, then we have cpt(Γ AF x (φ)(s), c 1 , c 2 ) * c 1 ,
and proceed with the reduction of c 1 , where cpt(Γ

AF x (φ)(s), c 1 , c 2 ) is a corresponding CPT of the sequent Γ AF x (φ)(s); - otherwise, AF x (φ)(s)
is added into the context, and for all s ∈ Next(s), we proceed with the reduction of a corresponding CPT of the sequent

Γ AF x (φ)(s ), where Γ = Γ ∪ {AF x (φ)(s)} 15 .
The example below illustrates the use and the abovementioned difference of merges in the CPT rewriting system. We apply the proof search method to the co-inductive formulae EG x (P(x))(a) and EG x (Q(x))(a) and to the inductive formulae AF x (¬P(x))(a) and AF x (Q(x))(a), respectively.

• The sequent EG x (P(x))(a) is provable in SCTL, and the CPT cpt( EG x (P(x))(a), t, f) reduces to t via the following rewriting steps:

cpt( EG x (P(x))(a), t, f) * cpt(Γ EG x (P(x))(b), t, cpt(Γ EG x (P(x))(c), t, f)) * cpt(Γ 1 EG x (P(x))(d), t, cpt(Γ EG x (P(x))(c), t, f)) * cpt(Γ 2 EG x (P(x))(d), t, cpt(Γ EG x (P(x))(c), t, f)) t where Γ = {EG x (P(x)(a))}, Γ 1 = Γ∪{EG x (P(x))(b)}, and Γ 2 = Γ 1 ∪ {EG x (P(x))(d)}. • The sequent EG x (Q(x))(a) is not provable in SCTL,
and the CPT cpt( EG x (Q(x))(a), t, f) reduces to f via the following rewriting steps:

cpt( EG x (Q(x))(a), t, f) cpt( Q(a), cpt(Γ EG x (Q(x))(b), t, cpt(Γ EG x (Q(x))(c), t, f)), f) f where Γ = {EG x (Q(x)(a))}. • The sequent AF x (¬P(x))(a)
is not provable in SCTL, and the CPT cpt( AF x (¬P(x))(a), t, f) reduces to f via the following rewriting steps:

where

Γ = {AF x (¬P(x)(a))}, Γ 1 = Γ ∪ {AF x (¬P(x))(b)}, and Γ 2 = Γ 1 ∪ {AF x (¬P(x))(d)}. • The sequent AF x (¬Q(x)(a)) is provable in SCTL,
and the CPT cpt( AF x (¬Q(x))(a), t, f) reduces to t via the following rewriting steps:

cpt( AF x (¬Q(x))(a), t, f) cpt( ¬Q(a), t, cpt(Γ AF x (¬Q(x))(b), cpt(Γ AF x (¬Q(x))(c), t, f), f)) t where Γ = {AF x (¬Q(x)(a))}.

Termination and correctness

To prove the termination of the CPT rewriting system, the following definitions are needed. DEFINITION 4.2 (Lexicographic path ordering [START_REF] Dershowitz | Termination of rewriting[END_REF][START_REF] Sarnat | Lexicographic path induction[END_REF]). Let F be a set of function symbols, where each element has a fixed arity and let be a quasi-ordering (i.e., a binary relation that is reflexive and transitive) on F. The lexicographic path ordering lpo on the set T (F) of terms over F is defined recursively as follows. s = f (s 1 , ..., s m ) lpo g(t 1 , ...,t n ) = t if and only if at least one of the following assertions holds:

1. s i lpo t for some i ∈ {1, ..., m}. 2. f g and s lpo t j for all j ∈ {1, ..., n}. 3. f = g and (s 1 , ..., s m ) lpo (t 1 , ...,t n ) and s lpo t j for all j ∈ {2, ..., n}, where lpo is the lexicographic ordering induced by lpo .

As usual, f g (resp. s lpo t) is shorthand for " f g and f = g" (resp. "s lpo t and s = t"). PROPOSITION 4.1 (Well-foundedness of lexicographic path orderings). Let be a quasi-ordering on a set F of function symbols where each element has a fixed arity, and lpo be the lexicographic path ordering on the set T (F) of terms over F. Then lpo is well-founded iff is.

Proof. See the proof proposed by Dershowitz [START_REF] Dershowitz | Termination of rewriting[END_REF]. It easy to check that, given a Kripke model, the weight of a sequent is well defined, and that the lexicographic order on the set of sequent weights induces a quasi-ordering on the set of sequents, which is well-founded.

THE COMPUTER JOURNAL, Vol. ??, No. ??, ???? PROPOSITION 4.2 (Termination). cpt( φ, t, f) always rewrites to t or f in finitely many steps.

Proof. Note first that, for any CPT c, if the rewriting of c is terminating, then it must end with either t or f. Now we prove that the rewriting of a CPT always terminates. Consider a CPT cpt( φ, t, f), we define first the set of functions symbols as follows:

F = {t, f, cpt} ∪ Seq
where Seq is the set of sequents that appear in the rewriting procedure of cpt( φ, t, f), cpt has arity 3, and other elements in F have arity 0. The quasi-ordering over F is defined as follows :

• cpt t; • cpt f; • Γ φ cpt for each sequent Γ φ; • Γ φ Γ φ iff w(Γ φ) > w(Γ φ ),
where > is the lexicographic order on pairs of natural numbers.

It is easy to check that is well-founded. By Definition 4.2, induces a lexicographic path ordering lpo on CPTs. By Proposition 4.1, lpo is also well-founded. Then it is sufficient to prove that, for any CPTs c and c ,

c c implies c lpo c .
We analyze each rule c c displayed in the CPT rewriting system. Suppose without loss of generality that c is in the form of cpt( φ, c 1 , c 2 ).

• If φ = , ⊥, P(s 1 , ..., s m ) or ¬P(s 1 , ..., s m ), then according to Definition 4.2 (1), we have

cpt (Γ φ, c 1 , c 2 ) lpo c 1 and c 2 because c 1 , c 2 are sub-terms of cpt(Γ φ, c 1 , c 2 ). • If φ = φ 1 ∧ φ 2 , then according to Definition 4.2 (3), we have cpt( φ 1 ∧ φ 2 , c 1 , c 2 ) lpo cpt( φ 1 , cpt( φ 2 , c 1 , c 2 ), c 2 ), because φ 1 ∧ φ 2 φ 1 , and cpt( φ 1 ∧ φ 2 , c 1 , c 2 ) lpo cpt( φ 2 , c 1 , c 2 ) and cpt( φ 1 ∧ φ 2 , c 1 , c 2 ) lpo c 2 . • If φ = φ 1 ∨ φ 2 , then according to Definition 4.2 (3), we have cpt( φ 1 ∨ φ 2 , c 1 , c 2 ) lpo cpt( φ 1 , c 1 , cpt( φ 2 , c 1 , c 2 )) because φ 1 ∨ φ 2 φ 1 , and cpt( φ 1 ∨ φ 2 , c 1 , c 2 ) lpo c 1 and cpt( φ 1 ∨ φ 2 , c 1 , c 2 ) lpo cpt( φ 2 , c 1 , c 2 ). • If φ = AX x (φ 1 )(s), then by Definition 4.2 (3), we have cpt(Γ AX x (φ 1 )(s), c 1 , c 2 ) lpo cpt( (s 1 /x)φ 1 , cpt(...cpt( (s n /x)φ 1 , c 1 , c 2 ), ..., c 2 ), c 2 ), because Γ AX x (φ 1 )(s) (s i /x)φ 1 , and cpt(Γ AX x (φ 1 )(s), c 1 , c 2 ) lpo cpt( (s i /x)φ 1 , cpt(...cpt( (s n /x)φ 1 , c 1 , c 2 )..., c 2 ), c 2 ), and cpt(Γ AX x (φ 1 )(s), c 1 , c 2 ) lpo c 2
, where Next(s) = {s 1 , ..., s n }, and i ∈ {1, ..., n}.

• The case of EX is analogous to that of AX.

• If φ = EG x (φ 1 )(s), consider the following cases:

- If EG x (φ 1 )(s) ∈ Γ, then by Definition 4.2 (1), we have cpt(Γ EG x (φ 1 )(s), c 1 , c 2 ) lpo c 1 .
-If EG x (φ 1 )(s) ∈ Γ, then by Definition 4.2 (3), we have c lpo c , as Γ EG x (φ 1 )(s) (s/x)φ 1 , and Γ EG x (φ 1 )(s) Γ EG x (φ 1 )(s i ) for all i ∈ {1, ..., n} where Next(s) = {s 1 , ..., s n }, and Γ = Γ ∪ {EG x (φ 1 )(s)}.

• The case of AF is analogous to that of EG.

• If φ = AR x,y (φ 1 , φ 2 )(s), consider the cases below:

- If AR x,y (φ 1 , φ 2 )(s) ∈ Γ, then by Definition 4.2 (1), we have cpt(Γ AR x,y (φ 1 , φ 2 )(s), c 1 , c 2 ) lpo c 1 . - If AR x,y (φ 1 , φ 2 )(s) / ∈ Γ, then by Definition 4.2 (3), we have, c lpo c because Γ AR x,y (φ 1 , φ 2 )(s) (s/y)φ 2 , Γ AR x,y (φ 1 , φ 2 )(s) (s/x)φ 1 , and Γ AR x,y (φ 1 , φ 2 )(s) Γ AR x,y (φ 1 , φ 2 )(s i ) for all i ∈ {1, ..., n}, where Next(s) = {s 1 , ..., s n }, and Γ = Γ ∪ {AR x,y (φ 1 , φ 2 )(s)}.
• The case of EU is analogous to that of AR.

The correctness of the proof search method is ensured by the following proposition. PROPOSITION 4.3 (Correctness). For any given closed formula φ, cpt( φ, t, f) * t if and only if φ is provable in SCTL.

Proof. The detailed proof is presented in Appendix D.

The proof search algorithm

Now we present the proof search algorithm, which is based on the CPT rewriting system. In this algorithm, much like in traditional model checking, we will store all the visited states (and the states currently been visited as well) in order to avoid visiting them several times, while keeping completeness. More precisely, in the proof search procedure of a formula φ, we use two global variables 16 (in the form of hash tables or BDDs) to store respectively the set of visited states on which a sub-formula of φ holds or not. This way, we avoid to visit repeatedly the states in these two global variables, and hence the repeated rewriting steps in the CPT rewriting system. The use of these two global variables is in fact an implementation of the merge rules. Note that this improvement does not break the termination property or the correctness property of the proof search method, as we omit repeated rewriting steps on CPTs only.

Thanks to an anonymous referee, we can use the example below to illustrate the application of the global variable storage above-mentioned. EXAMPLE 7. Consider a Kripke model that has 2n + 2 (n > 1) states: s 0 , s 1,1 , s 1,2 , ..., s 1,n-1 , s 1,n , s 2,0 , ..., s 2,n and a set P = {s 0 , s 1,1 , s 1,2 , ..., s 1,n-1 , s 2,0 , ..., s 2,n }, that is the property P holds at all states of this model except at state s 1,n . The graph of transition relation of this model is depicted as follows.

s 0 s 1,1 s 1,2 . . . s 1,n s 2,0 s 2,1 s 2,2 . . . s 2,n
When proving the formula EG x (P(x))(s 0 ), we need to rewrite the CPT cpt( EG x (P(x))(s 0 ), t, f). Suppose that s 1,1 is searched before s 2,0 in Next(s 0 ), and s 1,1 is searched before s 2,i+1 in Next(s 2,i ) for all i between 0 and n -1. The corresponding rewriting steps of the CPT are depicted in Figure 7,

FIGURE 7. Rewriting steps of cpt( EG x (P(x))(s 0 ), t, f)
where

Γ 0 = {EG x (P(x))(s 0 )}, Γ 1,i = {EG x (P(x))(s 0 ), EG x (P(x))(s 1,1 ), ..., EG x (P(x))(s 1,i )}, Γ 2,i = {EG x (P(x))(s 0 ), EG x (P(x))(s 2,0 ), ..., EG x (P(x))(s 2,i )}.
In Figure 7, before rewriting cpt(Γ 2,0 EG x (P(x))(s 2,1 ), t, f), all states in the path π = s 1,1 , s 1,2 , ..., s 1,n are already visited, and each time we rewrite cpt(Γ 2,i EG x (P(x))(s 2,i+1 ), t, f) (i ∈ {0, ..., n -1}), all states in π need to be visited one more time. That is because our proof search method is in a depth-first search style, When using a global variable M to store visited states, repeatedly visiting π can be avoided. Indeed, M stores all visited state s for which EG x (P(x))(s) does not hold, and before we rewrite cpt(Γ 2,i EG x (P(x))(s 2,i+1 ), t, f) (i ∈ {0, ..., n -1}), all states in π are already stored in M and hence no need to be visited again.

The pseudo code of the proof search algorithm is depicted in Figure 8, in which the notations are listed as follows.

• ψ denotes the sequent to be proved in SCTL. • c denotes the CPT to be rewritten.

• pt and ce denote the proof tree and counterexample to be constructed during the proof search, respectively. • M t (resp. M f ) is used to store the set of visited states on which a sub-formula of ψ holds (resp. does not hold), and they are used to avoid visiting the same state repeatedly. • visited is used to store temporally the visited states by sub-formula of ψ, starting with EU or AR (if any), and these states will be added into either M t or M f in later rewriting steps.

• We associate a set of actions A to each CPT c, written as c A . When rewriting a CPT c, each action in A needs to be performed. For instance, for a CPT c = cpt(Γ φ, c 1 , c 2 ), three sets of actions A 0 , A 1 , A 2 are associated to c, c 1 , c 2 , respectively. c A 0 is written as

cpt A 0 (Γ φ, c A 1 1 , c A 2 2
). When rewriting c, the actions in A 0 need to be performed. The actions in A 1 cannot be performed until c rewrites to c 1 . When rewriting c 1 , the actions in A 1 need to be performed. The case of c 2 is similar. Note that A 1 contains actions for constructing the proof tree of Γ φ, since we do not know if Γ φ is provable until c rewrites to c 1 ; while A 2 contains actions for constructing the counterexample, and each such an action cannot be performed unless c rewrites to c 2 .

There is a "while" loop in the pseudo code, which is to repeatedly rewrite the CPT c, until either t or f is reached. For the sake of brevity, only the subroutine ProveAnd is presented (Figure 9), where ac(t, parent, children) represents the operation of adding each element in children as a child to the node parent in the tree t. These operations are wrapped as actions in the pseudo code. The complete explanation of the pseudo code is in Appendix A.

A note on the complexity of the proof search algorithm. According to the proof search algorithm, for a given CPT cpt( φ, t, f), each sub-formula of φ appears, in the worst case, |M | times at the roots of CPTs that appear in the rewriting steps starting with cpt( φ, t, f), where |M | is the number of states in the Kripke model under consideration. Therefore, the time complexity of the proof search algorithm is O(|φ| × |M |), where |φ| is the size of the formula φ to be proved.

SCTLProV

In this section, we develop a new automated theorem prover called SCTLProV. 17 As is depicted in Figure 10, SCTLProV reads and interprets an input file containing a description of a Kripke model and a finite number of formulae -the properties (of this model) to be verified. It searches for a proof of each of these formulae and outputs a certificate (resp. True) when the verification succeeds, and a counterexample (resp. False), that is a proof of the negation of the formula, when it does not.

A note on the input language of SCTLProV. In the input languages of most traditional model checkers, a state in a Kripke model is usually expressed as a fixed number of values, and the types of these values are relatively simple, for instance, the Boolean data type, the integral data type, enumerated data types, etc. Such input languages usually cannot express complicated data structures such as linked lists with arbitrary finite length. In the input language of SCTLProV, the Kripke model is not always defined extensionally with a list of states and a list of transitions.

Input: An SCTL formula ψ. Output: A pair (r, t), where r is a Boolean, and t is either pt or ce.

1: function PROOFSEARCH 2: let c = cpt / 0 ( ψ, t / 0 , f / 0 ) 3:
let pt = ce = tree with a single node: ψ 4: let M t = M f = visited = empty hash table 5:

while c has the form cpt A 0 (Γ φ, c A 1 1 , c A 2 2 ) do 6:
∀a ∈ A 0 , perform action a 7:

case φ is 8:

: Here the type of states can be any datatype, in particular, it is easy to express linked lists with arbitrary finite length in the language, and the transitions are defined by an arbitrary computable function mapping a state to the list of its successors. This choice allows us to tackle, for instance, the SATS system, that is often difficult to solve for model checkers using a more extensional description of their input.

c := c A 1 1 9: ⊥: c := c A 2 2 10: P(s 1 , ..., s n ): 11: if s 1 , ..., s n ∈ P then c := c A 1 1 else c := c A 2 2 end if 12: ¬P(s 1 , ..., s n ): 13: if s 1 , ..., s n ∈ P then c := c A 2 2 else c := c A 1 1 end if 14: φ 1 ∧ φ 2 : ProveAnd( φ 1 ∧ φ 2 ) 15: φ 1 ∨ φ 2 : ProveOr( φ 1 ∨ φ 2 ) 16: EX x (φ 1 )(s) : ProveEX( EX x (φ 1 )(s)) 17: AX x (φ 1 )(s) : ProveAX( AX x (φ 1 )(s)) 18: EG x (φ 1 )(s) : ProveEG(Γ EG x (φ 1 )(s)) 19: AF x (φ 1 )(s) : ProveAF(Γ AF x (φ 1 )(s)) 20: EU x,y (φ 1 , φ 2 )(s) : ProveEU(Γ EU x,y (φ 1 , φ 2 )(s)) 21: AR x,y (φ 1 , φ 2 )(s) : ProveAR(Γ AR x,y (φ 1 , φ 2 )(s
A 12 = A 1 ∪ {ac(pt, φ 1 ∧ φ 2 , { φ 1 , φ 2 })} 2: let A 21 = A 2 ∪ {ac(ce, φ 1 ∧ φ 2 , { φ 1 })} 3: let A 22 = A 2 ∪ {ac(ce, φ 1 ∧ φ 2 , { φ 2 })} 4: let c = cpt / 0 ( φ 1 , cpt / 0 ( φ 2 , c A 12 1 , c A 22 2 ), c A 21 2 ) 5: c := c FIGURE 9. ProveAnd( φ 1 ∧ φ 2 ) Input file

Relations with some model checking techniques

Now we discuss the techniques adopted in SCTLProV with those in some other CTL model checking approaches. The verification procedure in SCTLProV differs from traditional CTL symbolic model checkers. For instance, unlike in NuSMV, there is no need for SCTLProV to calculate a fixed point of the transition relation. Instead, unfolding of the transition relation stops as soon as the given property is proved or refuted. Moreover, SCTLProV can store visited states either directly (using hash tables) when the model under consideration contains many non-Boolean variables, or using BDDs when the model contains mostly Boolean variables. In the latter case, unlike NuSMV that encodes models and properties into BDDs before searching state space, SCTLProV searches states directly on the Kripke model, using BDDs to store the visited states only.

On-the-fly model checking

The on-the-fly style of searching state space helps to avoid exploring unneeded states. Indeed, in an on-thefly model checker, there is usually no need to generate the full state space. Traditional on-the-fly CTL model checking algorithms [START_REF] Vergauwen | A linear local model checking algorithm for CTL[END_REF][START_REF] Bhat | Efficient on-the-fly model checking for ctl *[END_REF] are usually recursive, i.e., the unfolding of the formula and the transition rules are preformed recursively. These recursive based algorithms usually involve a lot of stack operations when verifying properties of large Kripke models. These stack operations may consume a lot of time and stack space during the verification processes.

In SCTLProV, the proof search of a formula mimics a double on-the-fly style model checking, that is, unfolding on demand both the transition relation of the given Kripke model and the formula to be verified. However, unlike traditional on-the-fly model checking algorithms, our algorithm is in continuation-passing style, which contains only constant stack operations [START_REF] Sestoft | Programming Language Concepts[END_REF]. In the programming language theory, a continuation is an explicit representation of the the rest of the computation. A function is said to be in continuation-passing style (CPS), if it takes an extra argument, the continuation, which decides what will happen THE COMPUTER JOURNAL, Vol. ??, No. ??, ???? to the result of the function. This method, usually used in compiling and programming, can help, among others, to reduce considerably the size of stacks [START_REF] Reynolds | The discoveries of continuations[END_REF][START_REF] Appel | Compiling with Continuations (corr. version)[END_REF][START_REF] Sestoft | Programming Language Concepts[END_REF].

We would like to compare our algorithm in SCTLProV to those given in [START_REF] Vergauwen | A linear local model checking algorithm for CTL[END_REF] and in [START_REF] Bhat | Efficient on-the-fly model checking for ctl *[END_REF], respectively. However, as far as we know, there are no tools based on these algorithms that can fully solve CTL model checking problems. To show that using continuation-passing style is not a trivial improvement, we designed specifically a recursion variant of SCTLProV, called SCTLProV R . 18 Unlike SCTLProV that uses continuations, SCTLProV R uses recursive calls to prove sub-formulae and search state space. We will compare the experimental results of SCTLProV and SCTLProV R in Section 6.2.

Bounded model checking

In traditional BMC tools, temporal formulae are unfolded on a set of traces with limited length once for all. For example, in model checking M , s 0 |= k+1 EFφ, one unfolding step of the EF formula involves k unfolding steps of the transition relation T , that is, BMC tools need to deal with the bulky formula [START_REF] Biere | Symbolic model checking without BDDs[END_REF]:

[M , EFφ] k+1 := k-1 i=0 T (s i , s i+1 ) ∧ k j=0 φ(s j )
To avoid exploring unnecessary states in M , SCTLProV unfolds on demand the transition relation T . Thus, in SCTLProV, one unfolding step of a formula involves at most one unfolding step of the transition relation. Indeed, to verify EF x (φ)(s 0 ), SCTLProV unfolds the transition relation T and the formula EF x (φ)(s 0 ) as

unfold(S, EF x (φ)(s i )) := φ(s i ) ∨ ((s i / ∈ S) ∧ T (s i , s i+1 ) ∧ unfold(S ∪ {s i }, EF x (φ)(s i+1 )))
where S is a set representing the visited states during the proof search, which is in fact the implementation of the merge rule of Figure 4.

SCTL AND FAIRNESS CONSTRAINTS

Fairness is an important aspect in verifying concurrent systems. Fairness assumptions often rule out unrealistic behaviors, and are often necessary to establish liveness properties [START_REF] Baier | Principles of Model Checking[END_REF]. For instance, in a mutual exclusion algorithm of two processes, we usually need to consider a fair scheduling of the execution of the processes, i.e., no process waits infinitely long. Such fairness constraints cannot be directly expressed in SCTL, since constraints over paths cannot be defined in SCTL. Here we define SCTL formulae under fairness constraints. Our definition of fairness coincides with that in [START_REF] Mcmillan | Symbolic Model checking[END_REF], i.e., the path quantifiers apply to those paths along which each formula in a given set holds infinitely often.

In the rest of this section, we suppose without loss of generality that a Kripke model is given implicitly.

We define the fairness constraint C as a finite set of SCTL formulae. An infinite path is fair under fairness constraint 18 https://github.com/sctlprov/sctlprov_r_code C if and only if, for each φ ∈ C, φ is valid infinitely often on this path. An SCTL formula EG x (φ)(t) under fairness constraint C, written as E C G x (φ)(t), is valid if and only if there exists an infinite path, fair under C, starting from state t such that for all state s on this path, (s/x)φ is valid. Similarly, an SCTL formula AF x (φ)(t) under fairness constraint C, written as A C F x (φ)(t), is valid if and only if for each infinite path, fair under C, starting from state t such that there exists a state s on this path and (s/x)φ is valid.

Similar to [START_REF] Mcmillan | Symbolic Model checking[END_REF], other SCTL formulae under fairness constraints can be characterized as follows:

E C X x (φ)(t) = EX x (φ ∧ E C G x ( )(x))(t) A C X x (φ)(t) = AX x (φ ∨ A C F x (⊥)(x))(t) E C U x,y (φ 1 , φ 2 )(t) = EU x,y (φ 1 , φ 2 ∧ E C G z ( )(y))(t) A C R x,y (φ 1 , φ 2 )(t) = AR x,y (φ 1 , φ 2 ∨ A C F z (⊥)(y))(t)
Since SCTL is sound and complete, to prove E C G x (φ)(t) is equivalent to prove EG x (φ)(t) where only fair paths are considered, i.e., to prove the existence of a fair path on which φ is always provable. Similarly, to prove A C F x (φ)(t) is equivalent to prove AF x (φ)(t) where only fair paths are considered, i.e., to prove the absence of a fair path on which φ can never be provable. Thus, to prove SCTL formulae under fairness constraints, we need a mechanism to decide the existence of fair paths. The merge rules in SCTL and Proposition 5.1 and 5.2 below ensure that we can decide the existence of a fair path in finitely many steps. To be more precise, when applying the merge rules, we check the fairness of the paths constructed and discard those that are not fair: i.e., we only consider merges where each formula in the given fairness constraint C is provable at some state of a cycle. PROPOSITION 5.1. Let C be a finite set of SCTL formulae and σ = s 0 , s 1 , ... be an infinite sequence of states such that s i -→ s i+1 for all i. If every element of C is valid infinitely often on σ, then there exists a finite sequence of states σ f = s 0 , s 1 , ..., s n such that

• each s j is a state on σ, • s j -→ s j+1 for all 0 ≤ j ≤ n -1, • s n = s p for some 0 ≤ p ≤ n -1,
• for every φ ∈ C, φ is valid at some state s q , where p ≤ q ≤ n .

Proof. As the number of states is finite, there exists a finite set of states S, such that each state in S appears infinitely often in σ, and each state not in S appears finitely often in σ. Then, each formula in C must be valid at some state in S, this is because otherwise, if there exists a formula φ ∈ C which is not valid on any state in S, then φ must be valid only finitely often on σ. Assume S = {s i 1 , s i 2 , ..., s i k } such that i 1 ≤ i 2 ≤ ... ≤ i k , then let σ f be a prefix of σ: σ f = s 0 , s 1 , ..., s n = s 0 , ..., s i 1 , ..., s i 2 , ..., s i k , ..., s i 1 , ..., s i 2 , ..., s i k . It is easy to check that all the requested conditions are satisfied. PROPOSITION 5.2. Let C be a finite set of SCTL formulae, and σ f = s 0 , s 1 , ..., s n be a finite sequence of states such that

• s i -→ s i+1 for all 0 ≤ i ≤ n -1,
• s p = s n for some 0 ≤ p ≤ n, • every formula in C is valid at some state between s p and s n in the sequence.

Then there exists an infinite sequence of states σ = s 0 , s 1 , ... such that

• each s j is a state on σ f , • s i -→ s i+1 for all i ≥ 0, • every formula in C is valid infinitely often on σ.

Proof. It is sufficient to take σ = s 0 , ..., s p-1 , s p , ..., s n-1 , s p , ..., s n-1 , ...

EXPERIMENTAL RESULTS AND APPLICA-TIONS

In this section, we discuss the feasibility and the efficiency of SCTLProV. First, we use a simple example to show the performance of SCTLProV, then we evaluate several benchmarks and compare the experimental results with the following verification tools: a Resolution-based theorem prover iProver Modulo All benchmarks used in this paper are available online. 19 All examples and benchmarks are tested on a Linux platform with 3.0 GB memory and a 2.93GHz × 4 CPU, and the time limit is 20 minutes. [START_REF] Peterson | Myths about the mutual exclusion problem[END_REF]). This example concerns a mutual exclusion algorithm of two concurrent processes (process A and process B). Mutual Exclusion means that at any time, the number of processes in the critical section is at most one. A sketch of the algorithm is depicted in Figure 11, where "flag" indicates that if there exists a process running at the moment, and "mutex" (has the initial value 0) is the number of processes that have entered the critical section. A violation of Mutual Exclusion means that at some state of the program, more than one process have entered the critical section, that is, the value of "mutex" is 2.

An illustrative example EXAMPLE 8 (A mutual exclusion problem

We use SCTLProV to check this algorithm.

The input file for this problem is depicted in Figure 12, where both the Kripke model and the property to be verified are defined. More precisely, two additional variables "a" and "b" are used to indicate the program counters of the two processes, respectively; "ini" stands for the initial state; "bug(s)" stands for the atomic formula meaning that at state "s" both process A and process B are in the critical section, that is, a bug of the algorithm is found at state "s"; and "find bug" stands for the property to be checked: from the initial state, a state "s" such that "bug(s)" holds is always reachable.

We check this property by using the following command.

sctl -output output.out mutual.model

The result is as follows, which indicates that the property "find bug" holds for the Kripke model, that is, the mutual exclusion property is violated in the model, and hence a bug is found in the algorithm above-mentioned.

verifying on the model mutual... find_bug: EU(x,y, TRUE, bug(y), ini) find_bug is true.

The output file "output.out" contains a proof tree of the verified property (Figure 13). Each node of the tree is in the form of id : seqt [id 1 , ..., id n ]

where seqt stands for a sequent, id the identity number of the sequent, and id 1 , ..., id n the identity numbers of the premises of the sequent.

THE COMPUTER JOURNAL, Vol. ??, No. ??, ???? This proof tree can be visualized by a visualization tool VMDV 20 (Visualization for Modeling, Demonstration, and Verification). VMDV is a 3D visualization tool for theorem provers, which provides interfaces for the integration with different theorem provers [START_REF] Liu | VMDV: A 3d visualization tool for modeling, demonstration, and verification[END_REF]. As depicted in Figure 14, we use in fact VMDV to visualize in 3D space both the proof tree and the Kripke model provided by SCTLProV , where the root node of the proof tree, containing the information about the verified property, is highlighted in red and so does the corresponding state (i.e., the initial state) in the Kripke model.

Note that the violation of the mutual exclusion property can be avoided if the algorithm is modified (Figure 15). We use SCTLProV to check the modified algorithm: the input file is depicted in Figure 16, where variable "x" and variable "y" are used to indicate that if process A and process B are running, respectively; and variable "turn" is used to indicate that it is whose turn to enter the critical section.

The output below shows that the modified algorithm is indeed a solution for the mutual exclusion exclusion problem.

verifying on the model mutual... find_bug: EU(x, y, TRUE, bug(y), ini) find_bug is false.

Randomly generated programs

We consider two benchmarks in this part. Benchmark #1 is originally proposed by Zhang [START_REF] Zhang | QBF encoding of temporal properties and QBF-based verification[END_REF]. Benchmark #2 is based on benchmark #1 by increasing the number of state variables. The randomness of the test cases in these benchmarks makes it rather fair for different CTL model checkers, and helps us understand the strengths and weaknesses of each of the tools.

Benchmark #1

Benchmark #1 was originally introduced by Zhang [START_REF] Zhang | QBF encoding of temporal properties and QBF-based verification[END_REF] in the evaluation of model checkers Verds and NuSMV, later, Ji [START_REF] Ji | CTL model checking in deduction modulo[END_REF] re-used it in the evaluation of the theorem prover iProver Modulo and the model checker Verds. For self containment of this paper, we briefly restate it here. This benchmark consists of 2880 randomly generated test cases where two types of random Boolean programs are considered-Concurrent Processes and Concurrent Sequential Processes.

Programs with Concurrent Processes. The parameters of the first set of random Boolean programs are as follows. t: number of transitions in a process p: number of parallel assignments in each transition For each Concurrent Sequential Process, in addition to b Boolean variables, there is a local variable representing the program location, which has c possible values. Each shared variable is initially set to a random value in {0, 1}, and each local variable is initially set to 0. For each transition of a process, p pairs of shared and local variables are randomly chosen among all variables, such that the first element of such a pair is set to the negation of the second element of the pair. Transitions are numbered from 0 to t -1, and are executed consecutively, and when the end of the sequence of the transitions is reached, it loops back to the execution of the transition numbered 0. For this type of programs, we test different sizes of the programs with 2 processes (a = 2), and let b vary in the set of values {12, 16, 20}, and then set c = b/2, d = c/a,t = c, and p = 4.

There are 24 properties to be checked in this benchmark: properties P 01 to P 12 are depicted in Table 1, and P 13 to P 24 are simply the variations of P 01 to P 12 by replacing ∧ and by ∨ and , respectively. In both programs with Concurrent Processes and programs with Concurrent Sequential Processes, each of 24 properties is tested on 20 test cases for each value of b.

P 01 AG( c i=1 v i ) P 02 AF( c i=1 v i ) P 03 AG(v 1 ⇒ AF(v 2 ∧ c i=3 v i )) P 04 AG(v 1 ⇒ EF(v 2 ∧ c i=3 v i )) P 05 EG(v 1 ⇒ AF(v 2 ∧ c i=3 v i )) P 06 EG(v 1 ⇒ EF(v 2 ∧ c i=3 v i )) P 07 AU(v 1 , AU(v 2 , c i=3 v i )) P 08 AU(v 1 , EU(v 2 , c i=3 v i )) P 09 AU(v 1 , AR(v 2 , c i=3 v i )) P 10 AU(v 1 , ER(v 2 , c i=3 v i )) P 11 AR(AXv 1 , AXAU(v 2 , c i=3 v i )) P 12 AR(EXv 1 , EXEU(v 2 , c i=3 v i ))

Experimental data

The experimental results for benchmark #1 and #2 are presented as follows. The interested reader is referred to Appendix B for the detailed data.

ing both with NuSMV and with NuXMV.

Table 2 shows the test cases (in benchmark#1 and #2) that can be solved by one and only one of the five tools. 21 For instance, the fourth line of the table shows that, among 480 test cases with Concurrent Processes, each having 48 state variables, there are 15 (3.1%) cases can only be solved by NuSMV or NuXMV, whereas 46 (9.6%) cases can only be solved by SCTLProV. To sum up, Table 2 shows that among 8640 test cases in benchmark #1 and #2, there are 61 (0.7%) cases that can only be solved by NuSMV or NuXMV, and 1250 (14.5%) cases can only be solved by SCTLProV.

It also shows that all test cases that are solvable by either iProver Modulo or Verds can be also solved by one of the other three tools. Figure 17 and Figure 18 show respectively that SCTL-ProV uses less time and space than the other four verification tools.

Continuation vs. recursion

To show the importance of using continuation-passing style in the proof search algorithm, we have implemented a recursive version of SCTLProV, denoted by SCTLProV R , and compared the time efficiency between them. In benchmark #1 and #2, SCTLProV solves about 10% more test cases than SCTLProV R , and it outperforms SCTLProV R in most solvable cases (Table 3). Indeed, SCTLProV R is more sensitive to the number of state variables than SCTLProV (Figure 19). REMARK 1. In the comparison of average verification time between SCTLProV and SCTLProV R , we extend the number of state variables in the case of Concurrent Sequential Processes by adding b = 52 and b = 72 in benchmark #2. 21 We do not make a distinction between the experimental data for NuSMV and for NuXMV, because they are almost the same.

Programs with fairness constraints

In this part, first we evaluate benchmark #3, which models mutual exclusion algorithms and ring algorithms 22 . Then, we compare the experimental results of SCTLProV, Verds, NuSMV, and NuXMV. We do not consider iProver Modulo here, because iProver Modulo cannot handle CTL properties under fairness constraints [START_REF] Ji | CTL model checking in deduction modulo[END_REF]. Benchmark #3 consists of two sets of concurrent programs: the mutual exclusion algorithms and the ring algorithms. Each kind of algorithms consists of a set of concurrent processes running in parallel.

In the mutual exclusion algorithms, the scheduling of processes is simple: for all i between 0 and n -2, process i + 1 performs a transition after process i, and process 0 performs a transition after process n-1. Each formula in the algorithms needs to be verified under the fairness constraint, that is, no process waits infinitely long.

Each process in the mutual exclusion algorithms has three internal states: noncritical, trying, and critical. The number of processes varies from 6 to 51. There are five properties specified by CTL formulae to be verified in mutual exclusion algorithms (Table 4). In these formulae, non i (resp. try i , cri i ) indicates that process p i has internal state noncritical (resp. trying, critical). According to the scheduling algorithm, processes 0 and 1 are not symmetric, as exemplified by the difference in performance between the properties P 4 and P 5 .

Each process in the ring algorithms consists of 5 Boolean internal variables indicating the internal state, and a Boolean variable indicating the output. Each process receives a Y. JIANG; J. LIU; G. DOWEK; AND K. JI Average verification time in SCTLProV vs. SCTLProV R

Prop

Mutual Exclusion Algorithms

P 1 EF(cri 0 ∧ cri 1 ) P 2 AG(try 0 ⇒ AF(cri 0 )) P 3 AG(try 1 ⇒ AF(cri 1 )) P 4 AG(cri 0 ⇒ Acri 0 U(¬cri 0 ∧ A¬cri 0 Ucri 1 )) P 5 AG(cri 1 ⇒ Acri 1 U(¬cri 1 ∧ A¬cri 1 Ucri 0 ))

TABLE 4. Properties to be verified in the mutual exclusion algorithms

Boolean value as the input during its running time. For a ring algorithm with processes p 0 , p 1 , ..., p n , the internal state of p i depends on the output of process p i-1 , and the output of p i-1 depends on its internal state, where 1 ≤ i ≤ n. The internal state of p 0 depends on the output of process p n , and the output of p n depends on the internal state of its own. The number of processes varies from 3 to 10. There are four properties specified by CTL formulae to be verified in ring algorithms (Table 5). In these formulae, out i indicates that the output of process p i is Boolean value true. The detailed experimental data for benchmark #3 are shown in Appendix B.3.

The VLTS benchmark

In this part, we evaluate benchmark #4, which is also called the VLTS (Very Large Transition Systems) benchmark 23 , which was originally proposed as a part of the CADP24 (Construction and Analysis of Distributed Processes) toolbox [START_REF] Garavel | CADP 2011: a toolbox for the construction and analysis of distributed processes[END_REF].

As a formal verification toolbox, CADP focuses on action-based models, for instance, Labeled Transition Systems (LTSs) and Markov Chains. As pointed out by the authors of CADP: this benchmark has been obtained from the modeling of various communication protocols and concurrent systems, many of which correspond to real life and industrial systems.

There are 40 test cases in benchmark #4, where deadlocks and livelocks are to be detected for each test case. All test cases in benchmark #4 are encoded in BCG (Binary-Coded Graphs) format, which is a binary format designed for encoding large state spaces [START_REF] Garavel | CADP 2011: a toolbox for the construction and analysis of distributed processes[END_REF]. When verifying test cases in this benchmark in SCTLProV, each BCG file was parsed into a Kripke model, and perform the proving procedure on the Kripke model. We compare the experimental results on benchmark #4 between SCTLProV and CADP.

Experimental data for benchmark #4. For 40 test cases in this benchmark, when detecting deadlocks, SCTLProV uses less time than CADP in 33 (82.5%) cases, and uses less memory than CADP in 7 (17.5%) cases; when detecting livelocks, SCTLProV uses less time than CADP in 22 (55%) cases, and uses less memory than CADP in 6 (15%) cases (Table 9). More details about the experiment on benchmark #4 are explained in Appendix B.4.

Discussion of the experimental results

In the evaluation of benchmark #1 to benchmark #3, the performances of NuSMV, NuXMV, Verds, iProver Modulo, and SCTLProV are affected by two factors: the number of state variables and the type of the property to be checked. The performances of NuSMV and NuXMV are mainly affected by the number of state variables, while the performances of iProver Modulo, Verds, and SCTLProV are mainly affected by the type of the property to be checked. When the number of state variables is rather small (such as in benchmark #1), NuSMV and NuXMV solves more test cases than iProver Modulo, Verds and SCTLProV, but when the number of state variables becomes larger (such as test cases in benchmark #2 and benchmark #3), the other three tools outperform them. On the other hand, when checking properties where nearly all states must be searched (such as AG properties), NuSMV and NuXMV usually perform better than iProver Modulo, Verds and SCTLProV. However, when checking the other properties (including some AG properties), iProver Modulo, Verds and SCTLProV are more efficient in time and in space, since they usually need to search and check much less states than NuSMV and NuXMV. To be precise, iProver Modulo, Verds and SCTLProV scale up better than NuSMV and NuXMV when checking these properties, and SCTLProV scales up better than both iProver Modulo and Verds, and outperforms them in most solvable cases.

In the evaluation of benchmark #4, the performances of SCTLProV and CADP are affected both by the number of states and the property to be checked. Moreover, SCTLProV runs faster than CADP in more than half of the test cases.

An application to the analysis of air traffic control protocols

As an application to an engineering problem, we present a concept of operations for the Small Aircraft Transportation System (SATS) [START_REF] Muñoz | Modeling and verification of an air traffic concept of operations[END_REF][START_REF]Abstract Model of SATS Concept of Operations: Initial Results and Recommendations[END_REF] in SCTLProV 25 .

In this concept of operations, the airspace volume surrounding an airport facility, called the self controlled area, is divided into 15 zones (Figure 20). For instance, the zone holding3(right) is a holding pattern at 3000 feet on the right side of the self controlled area. Each zone contains a list of aircraft and 24 transition rules that specify different SATS-procedures. For instance, the rule Vertical Entry (right) specifies the vertical entry of an aircraft in the zone holding3(right).

The model is non-deterministic, that is, for a given state, several transitions are possible and all must be considered. As there are no a priori bounds on the number of aircraft in each zone, the number of states in the model is potentially infinite. However, the number of states that are reachable FIGURE 20. SCA zones, where right and left are relative to the pilot facing the runway, i.e., opposite from the reader point of view [START_REF] Muñoz | Modeling and verification of an air traffic concept of operations[END_REF] from the initial state is finite: an enumeration of the model shows that there are 54221 such states (and around 3000 in the simplified model where departure operations are not considered [START_REF] Muñoz | Modeling and verification of an air traffic concept of operations[END_REF]).

There are eight properties of the model that we want to verify with SCTLProV, for instance that the SATS concept does not allow more than four simultaneous landing operations and none of the 15 zones contains too many aircraft (each zone is given a maximum number of aircraft and the actual number of aircraft is never higher than this number). The safety property is the conjunction of these eight properties.

The verification problem is to check that this property holds on every reachable state from the initial state (the state where there are no aircraft on each zone of the self controlled area), so the formula to be checked is AG x (φ)(e) where φ is the safety property and e is the initial state. This is a typical model checking problem, but this problem is known to be cumbersome for traditional model checkers [START_REF] Muñoz | Modeling and verification of an air traffic concept of operations[END_REF] because:

• Each state of the model is represented by a complex data structure. For instance, a number of state variables are represented by lists of aircraft with unbounded length.

• The transition rules of the model are represented by complex algorithms. For instance, some transitions rules involve recursive operations on lists of aircraft. • The properties to be verified in the model are also represented by complex algorithms. For instance, some of the properties are inductively defined over lists of aircraft.

However, this example fits well in SCTLProV which provides a more expressive input language than most traditional model checkers. Indeed, SCTLProV provides both readable notations for the definition of data structures such as records or lists with unbounded length, and arbitrary algorithms for the definitions of transition rules and of properties. So we have been able to check in SCTLProV that the safety property holds on every reachable state from the initial state in the model, and the verification was executed in less than 30 seconds on the same machine as which the benchmarks are evaluated.

CONCLUSION AND FUTURE WORKS

This paper provided a first step towards combining model checking and proof checking. We proposed a branchingtime logic CTL P which extends CTL with polyadic predicate symbols. CTL P permits not only to discuss properties of one fixed state, but also relations between different states. We designed then a proof system SCTL for CTL P , and developed a new automated theorem prover SCTLProV from scratch, tailored for SCTL. The particular aspects of SCTLProV are as follows: (1) it performs verification automatically and directly over any given Kripke model;

(2) in addition to generating counterexamples when the verification of the given property fails, SCTLProV permits to give a certificate for the property when it succeeds;

(3) it performs verification in a continuation-passing style and a doubly on-the-fly style, thanks to the syntax and inference rules of SCTL. In a nutshell, SCTLProV can be seen as either a theorem prover or a model checker, when solving CTL model checking problems, SCTLProV can give more instructive information than traditional model checkers, and can use more optimization strategies than traditional theorem provers.

As comparisons to other CTL model checking tools, we considered an automated theorem prover iProver Modulo, a QBF-based bounded model checker Verds, two BDDbased symbolic model checkers: NuSMV and its extension NuXMV, and a formal verification toolbox CADP. There are four benchmarks considered in the comparisons: benchmark #1 was originally introduced by Zhang [START_REF] Zhang | QBF encoding of temporal properties and QBF-based verification[END_REF] in the evaluation of Verds and NuSMV, and later, Ji [START_REF] Ji | CTL model checking in deduction modulo[END_REF] also used this benchmark in the evaluation of iProver Modulo and Verds; benchmark #2 was based on benchmark #1 by extending the number of state variables into tens, hundreds, and even thousands; benchmark #3 concerned verification with fairness constraints; benchmark #4 focused on deadlock and livelock detections. The experimental results show that SCTLProV performs well in terms of time and space consumption and can be considered complementary to model checkers such as NuSMV and NuXMV.

When applying SCTLProV on benchmark #4, LTSs have to be translated into Kripke models, which can increase considerably the number of states. Thus, the efficiency of SCTLProV can be further improved if the verification can perform directly over LTSs. One object of our future works is to design an SCTL-like proof system taking an LTS as the parameter.

So far, fairness constraints cannot be expressed in the syntax of CTL P nor in SCTL. Another object of our future works is to extend the logic and the proof system in order to formalize fairness constraints.

SCTLProV runs in a single-threaded mode. It seems not straightforward to extend it into a multi-threaded mode, because OCaml does not support thread-level parallelism. So the third object of our future works is to design a parallel version of SCTLProV.

actions in A 1 need to be performed. The case of c 2 is similar. Note that A 1 contains actions for constructing the proof tree of Γ φ, since we do not know if Γ φ is provable until c rewrites to c 1 ; while A 2 contains actions for constructing the counterexample, and each such an action cannot be performed unless c rewrites to c 2 .

There is a "while" loop in the pseudo code, which is to repeatedly rewrite the CPT c, until either t or f is reached. In the proof search algorithm, the rewriting steps for the cases where φ is an atomic formula or the negation of a atomic formula is presented, and the explanation for other cases are presented separately in the following Subsections.

Input: An SCTL formula ψ.

Output: A pair (r, t), where r is a Boolean, and t is either pt or ce.

1: function PROOFSEARCH 2: let c = cpt / 0 ( ψ, t / 0 , f / 0 ) 3:
let pt = ce = tree with a single node: ψ 4: let M t = M f = visited = empty hash table 5:

while c has the form cpt A 0 (Γ φ, c A 1 1 , c A 2 2 ) do 6:
∀a ∈ A 0 , perform action a 7:

case φ is 8:

:

c := c A 1 1 9: ⊥: c := c A 2 2 10: P(s 1 , ..., s n ): 11: if s 1 , ..., s n ∈ P then c := c A 1 1 else c := c A 2 2 end if 12: ¬P(s 1 , ..., s n ): 13: if s 1 , ..., s n ∈ P then c := c A 2 2 else c := c A 1 1 end if 14: φ 1 ∧ φ 2 : ProveAnd( φ 1 ∧ φ 2 ) 15: φ 1 ∨ φ 2 : ProveOr( φ 1 ∨ φ 2 ) 16:
EX x (φ 1 )(s) : ProveEX( EX x (φ 1 )(s)) 17:

AX x (φ 1 )(s) : ProveAX( AX x (φ 1 )(s)) 18:

EG x (φ 1 )(s) : ProveEG(Γ EG x (φ 1 )(s)) The pseudo code for the ProveAnd case is depicted in Figure A.2, where ac(t, parent, children) represents the operation of adding each element in children as a child to the node parent in the tree t. The pseudo code for this case is explained as follows.

• Line 4: When c 1 is reached from c in the future steps, both φ 1 and φ 2 are provable, then both φ 1 and φ 2 should be added as the children of φ 1 ∧ φ 2 in the proof tree (Line 1). Otherwise, if either of the inner or outer c 2 is reached from c , then the unprovability of either φ 1 (Line 2) or φ 2 (Line 3) is added as the evidence of negating φ 1 ∧ φ 2 in the counterexample.

• Line 5: Rewrite c to c . [START_REF] Baier | Principles of Model Checking[END_REF] shows the details of ProveOr, which is the dual case of ProveAnd.

1: let A 12 = A 1 ∪ {ac(pt, φ 1 ∧ φ 2 , { φ 1 , φ 2 })})} 2: let A 21 = A 2 ∪ {ac(ce, φ 1 ∧ φ 2 , { φ 1 })})} 3: let A 22 = A 2 ∪ {ac(ce, φ 1 ∧ φ 2 , { φ 2 })})} 4: let c = cpt / 0 ( φ 1 , cpt / 0 ( φ 2 , c A 12 1 , c A 22 2 ), c A 21 2 ) 5: c := c FIGURE A.2. ProveAnd( φ 1 ∧ φ 2 ) Figure A.
1: let A 22 = A 2 ∪ {ac(ce, φ 1 ∨ φ 2 , { φ 1 , φ 2 })})} 2: let A 11 = A 1 ∪ {ac(pt, φ 1 ∨ φ 2 , { φ 1 })})} 3: let A 12 = A 1 ∪ {ac(pt, φ 1 ∨ φ 2 , { φ 2 })})} 4: let c = cpt / 0 ( φ 1 , c A 11 1 , cpt / 0 ( φ 2 , c A 12 1 , c A 22 2 )) 5: c := c FIGURE A.3. ProveOr( φ 1 ∨ φ 2 ) Appendix A.2

. ProveEX and ProveAX

In the case of ProveEX, we let {s 1 , ..., s n } = Next(s), and the pseudo code for this case is depicted in Figure A.4. The analysis is analogous to that of Figure A.2, except that in Line 5 and Line 6, when c rewrites to the ith c 1 in the future steps, then (s i /x)φ 1 should be added as the children of EX x (φ 1 )(s) in the proof tree (Line 4), and otherwise, when c rewrites to c 2 , then (s 1 /x)φ 1 , ..., (s n /x)φ 1 should be added as the children of EX x (φ 1 )(s) in the counterexample (Line 3).

1: /* For notation purpose, here we refer "k" to EX x (φ 1 )( ), and 2: "k(s)" to EX x (φ 1 )(s).*/ 3: 1: /* For notation purpose, here we refer "k" to AX x (φ 1 )( ), and 2: "k(s)" to AX x (φ 1 )(s).*/ 3: 1: /* For notation purpose, here we refer "k" to EU x,y (φ 1 , φ 2 )( ) and 2: "k(s)" to EU x,y (φ 1 , φ 2 )(s).*/ 3: if s ∈ M t k then 4:

A 2 := A 2 ∪ {ac(ce, k(s), { (s 1 /x)φ 1 , ..., (s n /x)φ 1 })} 4: ∀i ∈ {1, ..., n}, let A 1i = A 1 ∪ {ac(pt, k(s), { (s i /x)φ 1 })} 5: let c = cpt / 0 ( (s 1 /x)φ 1 , c A 11 1 , cpt / 0 (...cpt / 0 ( (s n /x)φ 1 , c A 1n 1 , 6: c A 2 2 )...)) 7: c := c FIGURE A.4. ProveEX( EX x (φ 1 )(s))
A 1 := A 1 ∪ {ac(pt, k(s), { (s 1 /x)φ 1 , ..., (s n /x)φ 1 })} 4: ∀i ∈ {1, ..., n}, let A 2i = A 2 ∪ {ac(ce, k(s), { (s i /x)φ 1 })} 5: let c = cpt / 0 ( (
c := c A 1 1 5: M t k := M t k ∪ reachable(states(Γ)) 6: M f k := M f k \ reachable(states(Γ)) 7: else if s ∈ M f k or k(s) ∈ Γ then 8: c := c A 2
the size of the model increases.

To do so, we increase the number of variables in the random Boolean programs to {48, 60, 72, 252, 504, 1008} for Concurrent Processes, and {24, 28, 32, 252, 504, 1008} for Concurrent Sequential Processes, respectively. There are 5760 test cases in benchmark #2. Like in benchmark #1, all test cases in benchmark #2 are also randomly generated. The properties to be checked are the same as those in benchmark #1.

Counting the number of test cases that can be solved in 20 minutes, we see that SCTLProV scales up better (Table B Livelocks. Livelocks in LTSs are represented as cycles of one or more τ transitions. The detection of livelocks is more complex than deadlocks. The reason is that not only states, but also actions are to be examined in the exploration of the LTS.

It can be observed that for an LTS L and the Kripke model M by performing the above transformation on L, a livelock exists in L if and only if there exists a cycle of states where each state of the cycle satisfies Q. This is analyzed as follows.

→ • • • τ → s m τ → • • • τ → s p in L that is reachable from s 0 .
Thus, we can detect livelocks an LTS L by performing the proof search of the formula

EF x (EG y (Q(y))(x))((s 0 , •))
in the transformed Kripke model M . This formula is provable if and only if there exists a livelock in L. Proof. By induction on the structure of the proof π.

• If the last rule of π is atom-R, then the proved sequent has the form P(s 1 , ..., s n ), hence M |= P(s 1 , ..., s n ).

• If the last rule of π is ¬-R, then the proved sequent has the form ¬P(s 1 , ..., s n ), hence M |= ¬P(s 1 , ..., s n ).

• If the last rule of π is -R, the proved sequent has the form and hence M |= .

• If the last rule of π is ∧-R, then the proved sequent has the form φ 1 ∧ φ 2 . By induction hypothesis M |= φ 1 and M |= φ 2 , hence M |= φ 1 ∧ φ 2 .

• If the last rule of π is ∨-R 1 or ∨-R 2 , then the proved sequent has the form φ 1 ∨φ 2 . By induction hypothesis

M |= φ 1 or M |= φ 2 , hence M |= φ 1 ∨ φ 2 .
• If the last rule of π is AX-R, then the proved sequent has the form AX x (φ The path-tree |π| has root s, and for each leaf s of |π|, the sequent (s /x)φ 1 has a proof smaller than π. By induction hypothesis, for each leaf s of |π|, M |= (s /x)φ 1 . Hence M |= AF x (φ 1 )(s).

• If the last rule of π is EG-R, then the proved sequent has the form EG x (φ 1 )(s). We associate a finite sequence |π| to the proof π by induction in the following way.

-

If the proof π ends with the EG-merge rule, then the sequence contains a single element s.

-

If the proof π ends with the EG-R rule, with subproofs ρ and π 1 of the sequents (s/x)φ 1 and Γ, EG x (φ 1 )(s) EG x (φ 1 )(s ), respectively, then |π| is the sequence s|π 1 |.

The sequent |π| = s 0 , s 1 , ..., s n is such that s 0 = s; for all i between 0 and n -1, s i -→ s i+1 ; for all i between 0 and n, the sequent (s i /x)φ 1 has a proof smaller than π; and s n is equal to s p for some p between 0 and n-1. By induction hypothesis, for all i, we have M |= (s i /x)φ 1 .

Using Proposition 3.1, there exists an infinite sequence s 0 , s 1 , ... such that for all i, we have s i -→ s i+1 , and

M |= (s i /x)φ 1 . Hence, M |= EG x (φ 1 )(s).
• If the last rule of π is AR-R 1 or AR-R 2 , then the proved sequent has the form AR x (φ 1 , φ 2 )(s). We associate a finite path-tree |π| to the proof π by induction in the following way.

-If the proof π ends with the AR-R 1 rule with sub-proofs ρ 1 and ρ 2 of the sequents (s/x)φ 1 and (s/x)φ 2 , respectively, or with the AR-merge rule, then the path-tree contains a single node s.

-

If the proof π ends with the AR-R 2 rule, with sub-proofs ρ, π 1 , ..., π n of the sequents (s/y)φ 2 ,

Γ, AR x,y (φ 1 , φ 2 )(s) AR x,y (φ 1 , φ 2 )(s 1 ), ..., Γ, AR x,y (φ 1 , φ 2 )(s) AR x,y (φ 1 , φ 2 )(s n ), respec- tively, then |π| is the path-tree s(|π 1 |, ..., |π n |).
The path-tree |π| has root s, and for each node s of |π|, the sequent (s /y)φ 2 has a proof smaller than π; and for each leaf s , either the sequent (s /x)φ 1 has a proof smaller than π, or s is also a label of a node on the branch from the root of |π| to this leaf. By Y. JIANG; J. LIU; G. DOWEK; AND K. JI then it is sufficient to take the following proof tree as T .

T

1 φ 1 ∨ φ 2 ∨-R 1 2. cpt( φ 1 ∨ φ 2 , c 1 , c 2 ) cpt( φ 1 , c 1 , cpt( φ 2 , c 1 , c 2 )), cpt( φ 1 , c 1 , cpt( φ 2 , c 1 , c 2
)) rewrites to cpt( φ 2 , c 1 , c 2 ) before it rewrites to c 1 , and cpt( φ 2 , c 1 , c 2 ) rewrites to c 1 before it rewrites to c 2 . In this case, according to the induction hypothesis, φ 2 is provable. Suppose T 2 is the proof tree constructed for φ 2 , then it is sufficient to take the following proof tree as T .

T 2 φ 1 ∨ φ 2 ∨-R 2 • If Γ φ = EX x (φ 1 )(s)
, and {s 1 , ..., s n } = Next(s), then cpt( EX x (φ 1 )(s), c 1 , c 2 ) rewrites to c 1 before it rewrites to c 2 implies that there exists s i ∈ Next(s) such that (s i /x)φ 1 is provable. This is because otherwise, if for all s j ∈ Next(s), (s j /x)φ 1 is not provable, then according to the induction hypothesis,

cpt( EX x (φ 1 )(s), c 1 , c 2 ) cpt( (s 1 /x)φ 1 , c 1 , cpt(...cpt( (s n /x)φ 1 , c 1 , c 2 )...)) * cpt( (s n /x)φ 1 , c 1 , c 2 ) * c 2 ,
and c 1 has not been rewritten in the above rewriting steps. Suppose T is the proof tree constructed for (s i /x)φ 1 , then it is sufficient to take the following proof tree as T .

T EX x (φ 1 )(s)

EX-R

• If Γ φ = AX x (φ 1 )(s), as the dual case of EX, the analysis for the AX case is analogous to that of the EX case.

• If Γ φ = Γ EG x (φ 1 )(s), and {s 1 , ..., s n } = Next(s), then cpt(Γ EG x (φ 1 )(s), c 1 , c 2 ) rewrites to c 1 before it rewrites to c 2 implies that one of the following two cases holds.

1. EG x (φ 1 )(s) ∈ Γ; 2. EG x (φ 1 )(s) ∈ Γ, and cpt(Γ EG x (φ 1 )(s), c 1 , c 2 ) * cpt( (s/x)φ 1 , cpt(Γ EG x (φ 1 )(s 1 ), c 1 , cpt( ...cpt(Γ EG x (φ 1 )(s n ), c 1 , c 2 )...)), c 2 ) * cpt(Γ EG x (φ 1 )(s 1 ), c 1 , cpt(... cpt(Γ EG x (φ 1 )(s n ), c 1 , c 2 )...)) * cpt(Γ EG x (φ 1 )(s i ), c 1 , cpt(... cpt(Γ EG x (φ 1 )(s n ), c 1 , c 2 )...)) * c 1 , where Γ = Γ ∪ {EG x (φ 1 )(s)} and 1 ≤ i ≤ n.
If case 1 holds, then it is sufficient to take the following proof tree as T .

Γ EG x (φ 1 )(s)

EG-merge

If case 2 holds, then by induction hypothesis, both (s/x)φ 1 and Γ EG x (φ 1 )(s i ) are provable. Suppose T 1 and T 2 are the constructed proof trees of (s/x)φ 1 and Γ EG x (φ 1 )(s i ), respectively, then it is sufficient to take the following proof tree as T .

T 1 T 2 Γ EG x (φ 1 )(s)

EG-R

• If Γ φ = Γ AF x (φ 1 )(s), as the dual case of EG, the analysis for the AF case is analogous to that of the EG case.

• If Γ φ = Γ EU x,y (φ 1 , φ 2 )(s), {s 1 , ..., s n } =

• if φ is not an inductive formula, then Γ φ is provable implies that cpt(Γ φ, c 1 , c 2 ) rewrites to c 1 before it rewrites to c 2 ;

The proof of this proposition is by induction on the proof tree of Γ φ (Γ = / 0 when φ is an inductive formula).

• If the last rule in the proof tree is atom-R, then suppose φ = P(s 1 , ..., s n ) where P(s 1 , ..., s n ) is an atomic formula, and P(s 1 , ..., s n ) is provable, then s 1 , ..., s n ∈ P, then cpt( P(s 1 , ..., s n ), c 1 , c 2 ) c 1 . • If the last rule in the proof tree is ¬-R, then suppose φ = ¬P(s 1 , ..., s n ) where P(s 1 , ..., s n ) is an atomic formula, and ¬P(s 1 , ..., s n ) is provable, then s 1 , ..., s n / ∈ P, then cpt( ¬P(s 1 , ..., s n ), c 1 , c 2 ) c 1 .

• If the last rule in the proof tree is ∧-R, then suppose φ = φ 1 ∧ φ 2 and φ is provable, then according to the rules of the proof system, both φ 1 and φ 2 are provable, then according to the induction hypothesis, cpt( φ 1 ∧ φ 2 , c 1 , c 2 ) cpt( φ 1 , cpt( φ 2 , c 1 , c 2 ), c 2 ) * cpt( φ 2 , c 1 , c 2 ) * c 1 , and c 2 has not been rewritten in these rewriting steps.

• If the last rule in the proof tree is ∨-R, then φ = φ 1 ∨φ 2 and φ is provable, then according to the rules of the proof system, either φ 1 or φ 2 is provable:

1. if φ 1 is provable, then according to the induction hypothesis, cpt( φ 1 ∨ φ 2 , c 1 , c 2 ) cpt( φ 1 , c 1 , cpt( φ 2 , c 1 , c 2 )) * c 1 , and c 2 has not been rewritten in these rewriting steps; 2. if φ 1 is not provable but φ 2 is, then according to the induction hypothesis, either cpt( φ 1 ∨ φ 2 , c 1 , c 2 ) cpt( φ 1 , c 1 , cpt( φ 2 , c 1 , c 2 )) * c 1 , or cpt( φ 1 ∨ φ 2 , c 1 , c 2 ) cpt( φ 1 , c 1 , cpt( φ 2 , c 1 , c 2 )) * cpt( φ 2 , c 1 , c 2 ) * c 1 , and c 2 has not been rewritten in these rewriting steps.

• If the last rule in the proof tree is EX-R, then suppose φ = EX x (φ 1 )(s), {s 1 , ..., s n } = Next(s), and φ is provable, then according to the rules of the proof system, there exists s i ∈ Next(s) such that (s i /x)φ 1 is provable, and for all j such that 1 ≤ j < i, (s j /x)φ 1 is not provable. Then, according to the induction hypothesis, either cpt( EX x (φ 1 )(s), c 1 , c 2 ) cpt( (s 1 /x)φ 1 , c 1 , cpt(...cpt( (s n /x)φ 1 , c 1 , c 2 )...)) * cpt( (s j /x)φ 1 , c 1 , cpt(...cpt( (s n /x)φ 1 , c 1 , c 2 )...))

* c 1 where 1 ≤ j < i, or cpt( EX x (φ 1 )(s), c 1 , c 2 ) cpt( (s 1 /x)φ 1 , c 1 , cpt(...cpt( (s n /x)φ 1 , c 1 , c 2 )...)) * cpt( (s i /x)φ 1 , c 1 , cpt(...cpt( (s n /x)φ 1 , c 1 , c 2 )...))

* c 1 , and c 2 has not been rewritten in these rewriting steps.

• If the last rule in the proof tree is AX-R, then as the dual case of EX, the analysis for the AX case is analogous to that of the EX case.

• If the last rule in the proof tree is EG-R or EGmerge, then suppose φ = EG x (φ 1 )(s), {s 1 , ..., s n } = Next(s), and Γ EG x (φ 1 )(s) is provable, then either EG x (φ 1 )(s) ∈ Γ, or both (s/x)φ 1 and Γ EG x (φ 1 )(s i ) are provable, and Γ EG x (φ 1 )(s j ) is not provable for each j such that 1 ≤ j < i, where 1 ≤ i ≤ n and Γ = Γ ∪ {EG x (φ 1 )(s)}. In the former case, c rewrites to c 1 before it rewrites to c 2 . In the latter case, according to the induction hypothesis, either cpt(Γ EG x (φ 1 )(s), c 1 , c 2 ) cpt( (s/x)φ 1 , cpt(Γ EG x (φ 1 )(s 1 ), c 1 , cpt(... cpt(Γ EG x (φ 1 )(s n ), c 1 , c 2 )...)), c 2 ) * cpt(Γ EG x (φ 1 )(s 1 ), c 1 , cpt(... cpt(Γ EG x (φ 1 )(s n ), c 1 , c 2 )...)) * cpt(Γ EG x (φ 1 )(s j ), c 1 , cpt(...cpt(Γ EG x (φ 1 )(s n ), c 1 , c 2 )...)) * c 1 where 1 ≤ j < i, or cpt(Γ EG x (φ 1 )(s), c 1 , c 2 ) cpt( (s/x)φ 1 , cpt(Γ EG x (φ 1 )(s 1 ), c 1 , cpt(... cpt(Γ EG x (φ 1 )(s n ), c 1 , c 2 )...)), c 2 ) * cpt(Γ EG x (φ 1 )(s 1 ), c 1 , cpt(...cpt(Γ EG x (φ 1 )(s n ), c 1 , c 2 )...)) * cpt(Γ EG x (φ 1 )(s i ), c 1 , cpt(...cpt(Γ EG x (φ 1 )(s n ), c 1 , c 2 )...)) * c 1 , and c 2 has not been rewritten in these rewriting steps.

• If the last rule in the proof tree is AF-R 1 or AF-R 2 , then suppose φ = AF x (φ 1 )(s), {s 1 , ..., s n } = Next(s), and φ is provable, then either (s/x)φ 1 is provable, or AF x (φ 1 )(s i ) is provable for each 1 ≤ i ≤ n but (s/x)φ 1 is not provable. In the former case, by induction hypothesis, cpt( AF x (φ 1 )(s), c 1 , c 2 ) cpt( (s/x)φ 1 , c 1 , c 2 ) * c 1 for some c 2 and c 2 has not been rewritten in these rewriting steps. In the latter case, 1. if AF x (φ 1 )(s) labeled the root of a sub-proof of AF x (φ 1 )(s i ) for some 1 ≤ i ≤ n, then by induction hypothesis, cpt( AF x (φ 1 )(s), c 1 , c 2 ) rewrites to c 1 before it rewrites to c 2 since the proof of AF x (φ 1 )(s i ) contains a proof of AF x (φ 1 )(s); 2. otherwise, prune the proof of AF x (φ 1 )(s) such that all nodes in the proof tree are labeled by different sequents, and (s/x)φ 1 is not provable. By induction hypothesis, for all 1 ≤ i ≤ n, cpt( AF x (φ 1 )(s i ), c 1 , c 2 ) rewrites to c 1 before it rewrites to c 2 , then cpt(AF x (φ 1 )(s) AF x (φ 1 )(s i ), c 1 , c 2 ) must rewrite to c 1 before it rewrites to c 2 . This is because otherwise, if cpt(AF x (φ 1 )(s) AF x (φ 1 )(s i ), c 1 , c 2 ) rewrites to c 2 before it rewrites to c 1 , then according to the rewrite rules, there exists an infinite path s, s i , ..., s... such that for each state s in this path, (s /x)φ 1 is not provable, then according to the soundness and completeness of the proof system, AF x (φ 1 )(s i ) cannot be provable. Thus, cpt( AF x (φ 1 )(s), c 1 , c 2 ) cpt( (s/x)φ 1 , c 1 , cpt(AF x (φ 1 )(s 1 ), cpt(...cpt( AF x (φ 1 )(s n ), c 1 , c 2 )...), c 2 )) * cpt(AF x (φ 1 )(s 1 ), cpt(...cpt(AF x (φ 1 )(s n ), c 1 , c 2 )...), c 2 ) * cpt(AF x (φ 1 )(s n ), c 1 , c 2 ) * c 1 , and c 2 has not been rewritten in these rewriting steps.

• If the last rule in the proof tree is EU-R 1 or EU-R 2 , then suppose φ = EU x,y (φ 1 , φ 2 )(s), {s 1 , ..., s n } = Next(s), and φ is provable, then either (s/y)φ 2 is provable, or (s/y)φ 2 is not provable but both (s/x)φ 1 and EU x,y (φ 1 , φ 2 )(s i ) is provable for some 1 ≤ i ≤ n. In the former case, by induction hypothesis, cpt( EU x,y (φ 1 , φ 2 )(s), c 1 , c 2 ) cpt( (s/y)φ 2 , c 1 , c 2 ) * c 1 for some c 2 and c 2 has not been rewritten in these rewriting steps. In the latter case, 1. if EU x,y (φ 1 , φ 2 )(s) labeled the root of a subproof of EU x,y (φ 1 , φ 2 )(s i ), then by induction hypothesis, cpt( EU x,y (φ 1 , φ 2 )(s), c 1 , c 2 ) rewrites to c 1 before it rewrites to c 2 since we can find a smaller proof of EU x,y (φ 1 , φ 2 )(s) than that of EU x,y (φ 1 , φ 2 )(s i ); 2. otherwise, prune the proof tree of EU x,y (φ 1 , φ 2 )(s) such that all nodes in the proof tree are labeled by different sequents. Then, there exists 1 ≤ i ≤ n such that cpt(EU x,y (φ 1 , φ 2 )(s) EU x,y (φ 1 , φ 2 )(s i ), c 1 , c 2 ) rewrites to c 1 before it rewrites to c 2 . This is because otherwise, if for all 1 ≤ i ≤ n, cpt(EU x,y (φ 1 , φ 2 )(s) EU x,y (φ 1 , φ 2 )(s i ), c 1 , c 2 ) rewrites to c 2 before it rewrites to c 1 , then according to the rewrite rules, each branch of states searched is either of the form s, s i , ..., s where (s /y)φ 2 is not provable for each state s of the path, or of the form s, s i , ..., s where (s /x)φ 1 is not provable and (s /y)φ 2 is not provable for every state s of the path, and thus according to the soundness and completeness of the proof system, EU x,y (φ 1 , φ 2 )(s i ) cannot be provable for each 1 ≤ i ≤ n. Thus, there exists 1 ≤ i ≤ n such that cpt(EU x,y (φ 1 , φ 2 )(s) EU x,y (φ 1 , φ 2 )(s i ), c 1 , c 2 ) rewrites to c 1 before it rewrites to c 2 . Then, cpt( EU x,y (φ 1 , φ 2 )(s), c 1 , c 2 ) cpt( (s/y)φ 2 , c 1 , cpt( (s/x)φ 1 , cpt( EU x,y (φ 1 , φ 2 )(s) EU x,y (φ 1 , φ 2 1 ), c 1 , cpt(... cpt(EU x,y (φ 1 , φ 2 )(s) EU x,y (φ 1 , φ 2 )(s n ), c 1 , c 2 )... )), c 2 )) * cpt(EU x,y (φ 1 , φ 2 )(s) EU x,y (φ 1 , φ 2 )(s 1 ), c 1 , cpt(...cpt(EU x,y (φ 1 , φ 2 )(s) EU x,y (φ 1 , φ 2 )(s n ), c 1 , c 2 )...)) * cpt(EU x,y (φ 1 , φ 2 )(s) EU x,y (φ 1 , φ 2 )(s i ), c 1 , cpt(...cpt(EU x,y (φ 1 , φ 2 )(s) EU x,y (φ 1 , φ 2 )(s n ), c 1 , c 2 )...)) * c 1 , and c 2 has not been rewritten in these rewriting steps.

• If the last rule in the proof tree is AR-R 1 , AR-R 2 , or AR-merge, then suppose φ = AR x,y (φ 1 , φ 2 )(s), {s 1 , ..., s n } ∈ Next(s), and Γ AR x,y (φ 1 , φ 2 )(s) is provable, then at least one of the following three assertions holds, where Γ = Γ ∪ {AR x,y (φ 1 , φ 2 )(s)}.

1. AR x,y (φ 1 , φ 2 )(s) ∈ Γ. In this case, cpt(Γ AR x,y (φ 1 , φ 2 )(s), c 1 , c 2 ) c 1 .

2. Both (s/x)φ 1 and (s/y)φ 2 are provable. In this case, according to the induction hypothesis, cpt(Γ AR x,y (φ 1 , φ 2 )(s), c 1 , c 2 ) * cpt( (s/y)φ 2 , cpt( (s/x)φ 1 , c 1 , cpt(Γ AR x,y (φ 1 , φ 2 )(s 1 ), cpt(...cpt( Γ AR x,y (φ 1 , φ 2 )(s n ), c 1 , c 2 )...), c 2 )), c 2 ) * c 1 , and c 2 has not been rewritten in these rewriting steps.

3.

(s/y)φ 2 is provable, and that Γ AR x,y (φ 1 , φ 2 )(s i ) is provable for each s i ∈ Next(s). In this case, according to the induction hypothesis, cpt(Γ AR x,y (φ 1 , φ 2 )(s), c 1 , c 2 ) * cpt( (s/y)φ 2 , cpt( (s/x)φ 1 , c 1 , cpt(Γ AR x,y (φ 1 , φ 2 )(s 1 ), cpt(...cpt( Γ AR x,y (φ 1 , φ 2 )(s n ), c 1 , c 2 )...), c 2 )), c 2 ) * cpt(Γ AR x,y (φ 1 , φ 2 )(s 1 ), cpt(...cpt( Γ AR x,y (φ 1 , φ 2 )(s n ), c 1 , c 2 )...), c 2 ) * cpt(Γ AR x,y (φ 1 , φ 2 )(s n ), c 1 , c 2 ) * c 1 , and c 2 has not been rewritten in these rewriting steps.

Thus, cpt(Γ AR x,y (φ 1 , φ 2 )(s), c 1 , c 2 ) rewrites to c 1 before it rewrites to c 2 .

DEFINITION 2 . 1 (

 21 Kripke model).A Kripke model M is given by

FIGURE 1 .

 1 FIGURE 1. Validity of a formula in CTL P

FIGURE 2 .

 2 FIGURE 2. Possible positions of an unmanned vehicle

{s 1 ,

 1 ...s n }=Next(s) EXAMPLE 3. Consider the Kripke model formed with the following relation and the set P = {b, c}. the formula AF x (P(x))(a) is

THEOREM 3 . 1 (

 31 Soundness and completeness). If φ is closed, then the sequent φ has a proof in SCTL(M ) if and only if M |= φ for the given Kripke model M . Proof. The soundness and completeness are guaranteed by the finiteness of the Kripke model and Proposition 3.1, 3.2, 3.3 and 3.4 above-mentioned. The details are presented in Appendix C.

DEFINITION

EXAMPLE 6 .

 6 Consider the Kripke model formed with the following relation and two sets P = {a, b, d} and Q = {b, c}.

DEFINITION 4 . 3 (

 43 Weight of a sequent). Given a Kripke model M with cardinal n and a sequent Γ φ in SCTL(M ), let |φ| denote the size of φ defined in the usual way, and |Γ| denote the cardinal of a context Γ. We define the weight of the sequent Γ φ as w(Γ φ) = |φ|, (n -|Γ|)

  [START_REF] Burel | Experimenting with deduction modulo[END_REF], a QBF-based bounded model checker Verds (version 1.49), a BDD-based unbounded model checker NuSMV (version 2.6.0) and its extension NuXMV (version 1.0.0), and a formal verification toolbox CADP. Finally, we apply SCTLProV to a safety problem in air traffic control.

FIGURE 11 .FIGURE 12 .

 1112 FIGURE 11. A sketch of process A and process B Model mutual() { Var { flag : Bool; mutex : (0 .. 2); a : (1 .. 5); b : (1 .. 5); } Init { flag := false; mutex := 0; a := 1; b := 1; } Transition { a = 1 && flag = false : {a := 2;}; a = 2 : {a := 3; flag := true;}; / * A has entered the critical section * / a = 3 : {a := 4; mutex := mutex + 1;}; / * A has left the critical section * / a = 4 : {a := 5; mutex := mutex -1;}; a = 5 : {flag := 0;}; b = 1 && flag = false : {b := 2;}; b = 2 : {b := 3; flag := true;}; / * B has entered the critical section * / b = 3 : {b := 4; mutex := mutex + 1;}; / * B has left the critical section * / b = 4 : {b := 5; mutex := mutex -1;}; b = 5 : {flag := 0;}; / * If none of the conditions above are satisfied, then the current state goes to itself. * / (a = 1 || b = 1) && flag = true: {} } Atomic {bug(s) := s(mutex = 2);} Spec{find_bug := EU(x, y, TRUE, bug(y), ini);} }

FIGURE 13 .

 13 FIGURE 13. The output file "output.out"

FIGURE 14 .FIGURE 15 .

 1415 FIGURE 14. Visualization of the proof tree and the Kripke model in the illustrative example

FIGURE 16 .

 16 FIGURE 16. The input file for the modified algorithm

FIGURE 17 .

 17 FIGURE 17. Average verification time in benchmark #1 and #2

  FIGURE 19.Average verification time in SCTLProV vs. SCTLProV R

FIGURE A. 1 .

 1 FIGURE A.1. The proof search algorithm

Figure A. 5

 5 Figure A.5 shows the details of ProveAX, which is the dual case of ProveEX.

Figure A. 9

 9 Figure A.9 shows the details of ProveAR, which is the dual case of ProveEU.

•

  (⇒) If there exists a cycle of τ transitions in L, then the cycle has the form s p τ → s p+1 τ → • • • τ → s n τ → s p , where either s p = s 0 , or there exists a path s 0 a 0 → • • • a p-1 → s p . Then according to the transformation, there exists a cycle of the form (s p , a) -→ (s p+1 , τ) -→ • • • -→ (s n , τ) -→ (s p , τ) -→ (s p+1 , τ) in M , where (s 0 , •) -→ * (s p , a), and a = a p-1 .

  , c 2 ) c 1 cpt( ⊥, c 1 , c 2 ) c 2 cpt( P(s 1 , ..., s n ), c 1 , c 2 ) c 1 [ s 1 , ..., s n ∈ P] cpt( P(s 1 , ..., s n ), c 1 , c 2 ) c 2 [ s 1 , ..., s n / ∈ P] cpt( ¬P(s 1 , ..., s n ), c 1 , c 2 ) c 2 [s 1 , ..., s n ∈ P] cpt( ¬P(s 1 , ..., s n

	cpt(	, c 1
		4.1	(Continuation-passing	tree). A
		continuation-passing tree (CPT for short) is a binary
		tree such that
		• every leaf is labeled by either t or f, where t and f are
		THE COMPUTER JOURNAL, Vol. ??, No. ??, ????

  4.4.1. BDD-based symbolic model checking When a Kripke model contains mostly Boolean variables, for instance in model checking for hardware problems, using BDDs to store states is an effective way to reduce space occupation during the verification procedure. The best known BDD-based symbolic model checker is NuSMV [29, 30], as well as its extension NuXMV [31]. To illustrate the verification procedure in a BDD-based symbolic model checker, let us consider, for instance, a Kripke model M with the initial state s 0 and a transition relation T . To check whether M , s 0 |= EFφ holds in such a model checker,say NuSMV, first one needs to calculate the least fixed point lfp = µY.(φ ∨ EXY ), then check whether s 0 ∈ lfp[START_REF] Mcmillan | Symbolic Model checking[END_REF][START_REF] Cimatti | Nusmv: A new symbolic model verifier[END_REF]. Calculating lfp corresponds to unfolding the transition relation T , where states that are not reachable from s 0 may be involved.

TABLE 1 .

 1 Properties P 01 , P 02 , . . . , P 12 to be checked in benchmark #1 and #2

	6.2.2. Benchmark #2
	In benchmark #2, the value of b in benchmark #1 is increased
	to {48, 60, 72, 252, 504, 1008} for Concurrent Processes,
	and {24, 28, 32, 252, 504, 1008} for Concurrent Sequential
	Processes, respectively. There are 5760 test cases in
	benchmark #2. Like in benchmark #1, all test cases in
	benchmark #2 are also randomly generated. The properties
	to be checked are the same as those in benchmark #1.

TABLE 2 .

 2 Test cases in benchmark #1 and #2 that can be solved by one and only one of the five tools

TABLE 3 .

 3 SCTLProV vs. SCTLProV R

TABLE 5 .

 5 Properties to be verified in the ring algorithmsExperimental data for benchmark #3. Among 262 test cases in this benchmark, Verds can solve 168 (64.1%) cases, both NuSMV and NuXMV can solve 71 (27.1%) cases, and SCTLProV can solve 211 (80.2%) cases (Table6). There are 194 (74.0%) test cases on which SCTLProV runs faster and uses less memory comparing with Verds, and 211 (80.2%) comparing both with NuSMV and with NuXMV (Table7).

	Prop	Ring Algorithms
	P 1		AGAFout 0 ∧ AGAF¬out 0
	P 2		AGEFout 0 ∧ AGEF¬out 0
	P 3		EGAFout 0 ∧ EGAF¬out 0
	P 4		EGEFout 0 ∧ EGEF¬out 0
	Programs		Verds	NuSMV	NuXMV SCTLProV
	mutual exclusion 136 (59.1%) 50 (21.7%) 50 (21.7%) 191 (83.0%)
	ring		32 (100%) 21 (65.6%) 21 (65.6%) 20 (62.5%)
	Sum	168 (64.1%) 71 (27.1%) 71 (27.1%) 211 (80.2%)

TABLE 6 .

 6 The solvable cases in Verds, NuSMV, NuXMV, and SCTLProV Table8shows the test cases in benchmark #3 that can be solved by one and only one of the four tools. There are 5 (1.9%) test cases that can only be solved by Verds, and there are 66 (25.2%) test cases that can only be solved by

	Programs	Verds	NuSMV	NuXMV
	mutual exclusion 187 (81.3%) 191 (83.0%) 191 (83.0%)
	ring	7 (21.9%) 20 (62.5%) 20 (62.5%)
	Sum	194 (74.0%) 211 (80.2%) 211 (80.2%)

TABLE 7 .

 7 The test cases where SCTLProV both runs faster and uses less memory than Verds, NuSMV, and NuXMV, respectively SCTLProV. There is no test case that can only be solved by NuSMV or by NuXMV.

	Programs	Verds NuSMV/NuXMV SCTLProV
	mutual exclusion	0	0 66 (28.7%)
	ring	5 (15.6%)	0	0
	Sum	5 (1.9%)	0 66 (25.2%)

TABLE 8 .

 8 Test cases that can be solved by one and only one of the four tools

TABLE 9 .

 9 Test

cases where SCTLProV uses less time and less memory than CADP, respectively

  (s/x)φ 1 and Γ EU x,y (φ 1 , φ 2 )(s i ) are provable, and thus these two sequents are added to the proof tree as the children of Γ EU x,y (φ 1 , φ 2 )(s) (Line 19 -20). 3. If c rewrites to the outer c 2 , then both (s/x)φ 1 and (s/y)φ 2 should be added to the counterexample as the children of Γ EU x,y (φ 1 , φ 2 )(s) If c rewrites to the inner c 2 , thenΓ EU x,y (φ 1 , φ 2 )(s 1 ), ..., Γ EU x,y (φ 1 , φ 2 )(s n )should all be added to the counterexample as the children of Γ EU x,y (φ 1 , φ 2 )(s) (Line 18). • Line 28: Rewrite c to c .

	(Line 16).	At the same time, all states
	in states(Γ) ∪ {s} should be added into
	M f EU x,y (φ 1 ,φ 2 )( ) to avoid being visited again
	(Line 17).
	4.
		6:	c A 21 2 )	s 1 /x)φ, cpt / 0 (...cpt / 0 ( (s n /x)φ, c A 1 1 , c A 2n 2 ), ...),
		7: c := c
				FIGURE A.5. ProveAX( AX x (φ 1 )(s))
		THE COMPUTER JOURNAL, Vol. ??, No. ??, ????

  .3, Table B.4) than the other four tools: SCTLProV solves more test cases than the other tools, and SCTLProV outperforms the other tools in most solvable test cases.

	Programs	iProver Modulo	Verds	NuXMV	NuXMV	SCTLProV
	CP (b = 48)	375 (78.1%)	400 (83.3%) 171 (35.6%) 176 (36.7%)	446(92.9%)
	CP (b = 60)	360 (75.0%)	403 (84.0%)	22 (4.6%)	23 (4.8%)	440(91.7%)
	CP (b = 72)	347 (72.3%)	383 (79.8%)	0	0	437 (91.0%)
	CP (b = 252)	299 (62.3%)	216 (45.0%)	0	0	371 (77.3%)
	CP (b = 504)	292 (60.8%)	0	0	0	335 (69.8%)
	CP (b = 1008)	271 (56.5%)	0	0	0	278 (57.9%)
	CSP (b = 24)	190 (39.6%)	235 (49.0%) 421 (87.7%) 423 (88.1%)	430 (89.6%)
	CSP (b = 28)	172 (35.8%)	229 (47.7%) 106 (22.1%) 108 (22.5%)	426 (88.8%)
	CSP (b = 32)	158 (32.9%)	224 (46.7%)	8 (1.7%)	6 (1.3%)	418 (87.1%)
	CSP (b = 252)	114 (23.6%)	136 (28.3%)	0	0	312 (65.0%)
	CSP (b = 504)	108 (22.5%)	0	0	0	295 (61.5%)
	CSP (b = 1008)	62 (12.9%)	0	0	0	253 (52.7%)
	Sum	2748 (47.7%) 2226 (38.6%) 728 (12.6%) 736 (12.8%) 4441 (77.1%)

TABLE B . 3 .

 B3 Solvable cases in five tools

	Programs	iProver Modulo	Verds	NuSMV	NuXMV
	CP (b = 48)	446 (92.9%)	444 (92.5%)	442 (92.1%)	442 (92.1%)
	CP (b = 60)	440 (91.7%)	440 (91.7%)	440 (91.7%)	440 (91.7%)
	CP (b = 72)	437 (91.0%)	437 (91.0%)	437 (91.0%)	437 (91.0%)
	CP (b = 252)	371 (77.3%)	371 (77.3%)	371 (77.3%)	371 (77.3%)
	CP (b = 504)	335 (69.8%)	335 (69.8%)	335 (69.8%)	335 (69.8%)
	CP (b = 1008)	278 (57.9%)	278 (57.9%)	278 (57.9%)	278 (57.9%)
	CSP (b = 24)	430 (89.6%)	429 (89.4%)	426 (88.8%)	426 (88.8%)
	CSP (b = 28)	426 (88.8%)	426 (88.8%)	425 (88.5%)	425 (88.5%)
	CSP (b = 32)	418 (87.1%)	418 (87.1%)	418 (87.1%)	418 (87.1%)
	CSP (b = 252)	312 (65.0%)	312 (65.0%)	312 (65.0%)	312 (65.0%)
	CSP (b = 504)	295 (61.5%)	295 (61.5%)	295 (61.5%)	295 (61.5%)
	CSP (b = 1008)	253 (52.7%)	253 (52.7%)	253 (52.7%)	253 (52.7%)
	Sum	4441 (77.1%) 4438 (77.0%) 4432 (76.9%) 4432 (76.9%)

TABLE B . 4 .

 B4 Cases where SCTLProV runs faster than iProver Modulo, Verds, NuSMV, and NuXMV, respectively transition (s, a) -→ (s d , •) to M ; • Finally, let P = {(s d , •)} and Q = {(s, τ) ∈ S | s ∈ S}. Note that in the above transformation, we add a special state (s d , •) to the transformed Kripke model, where s d / ∈ S and • / ∈ Act. Also, for every state (s, a) ∈ S where s has no successor in the LTS to be transformed, add a special transition (s, a) -→ (s d , •) to the transformed Kripke model; and to make the transition relation -→ total, we add another special transition (s d , •) -→ (s d , •) to the transformed Kripke model. The addition of the special state and transitions are necessary in this transformation. It is because otherwise, the transformed structure may not be called a Kripke model, since there may exist states that have no successors.Then, we explain that the existence of deadlocks and livelocks in LTSs can be detected by performing the following verifications in the transformed Kripke models.Deadlocks. A deadlock state in an LTS is a state which has no successor. When detecting deadlocks of an LTS L in SCTLProV, we first translate L into a Kripke model M using the above transformation. It can be observed that a deadlock state is reachable from s 0 in L if and only if (s d , •) is reachable from (s 0 , •) in M . Thus, we can detect deadlocks in an LTS L by performing the proof search of the formula EF x (P(x))((s 0 , •)) in the transformed Kripke model M . This formula is provable if and only if (s 0 , •) -→ * (s, a) -→ (s d , •), where a is an action, and s has no successor in L. Thus, the proof search of the formula can be used to detect deadlocks in L. perform the deadlock detection both in SCTLProV and CADP on this benchmark. For 40 test cases in this benchmark, both SCTLProV and CADP can solve all test cases. Moreover, SCTLProV uses less time than CADP in 33 (82.5%) test cases, and uses less memory than CADP in 7 (17.5%) test cases. The detailed experimental data is depicted in Table B.6.

	We

TABLE B .

 B

	a 0 → • • •

6. Deadlock detection in SCTLProV and CADP • (⇐) If there exists a cycle of the form (s p , τ) -→ (s p+1 , τ) -→ • • • -→ (s n , τ) -→ (s p , τ) which is reachable from (s 0 , •) in M , then (s 0 , •) -→ * (s m , τ) for some (s m , τ) in the cycle, then we have s 0 a → s τ → s m in L, and there exists a cycle s p τ

  We perform the livelock detection both in SCTLProV and CADP on this benchmark. For 40 test cases in this benchmark, both SCTLProV and CADP can solve all test cases. Moreover, SCTLProV uses less time than CADP in 22 (55%) test cases, and uses less memory than CADP in 6 (15%) test cases. The detailed experimental data is depicted in Table B.7.

	Name	Livelocks	SCTLProV sec MB	CADP sec	MB
	vasy 0 1	No	0.13	27.45	0.48	14.57
	cwi 1 2	No	0.14	27.74	0.50	14.61
	vasy 1 4	No	0.14	27.70	0.48	14.66
	cwi 3 14	No	0.16	28.18	0.50	14.57
	vasy 5 9	No	0.16	28.08	0.51	14.68
	vasy 8 24	No	0.18	29.09	0.53	14.75
	vasy 8 38	No	0.20	28.86	0.52	14.73
	vasy 10 56	No	0.23	30.33	0.55	15.34
	vasy 18 73	No	0.28	33.07	0.56	16.25
	vasy 25 25	No	1.12	33.45	2.25	27.84
	vasy 40 60	No	0.26	30.23	0.57	19.65
	vasy 52 318	Yes	0.21	27.66	0.55	15.45
	vasy 65 2621	No	5.31	280.57	1.98	113.40
	vasy 66 1302	No	2.40	38.33	1.30	18.50
	vasy 69 520	No	1.04	33.41	0.85	16.39
	vasy 83 325	No	0.83	39.27	0.76	19.40
	vasy 116 368	No	1.19	42.14	0.86	15.74
	cwi 142 925	No	2.67	46.30	1.22	17.89
	vasy 157 297	No	0.80	33.99	0.78	17.91
	vasy 164 1619	No	3.69	53.30	1.51	23.44
	vasy 166 651	No	1.60	49.98	1.02	26.02
	cwi 214 684	Yes	0.26	29.93	0.63	16.81
	cwi 371 641	Yes	0.26	30.63	0.62	17.41
	vasy 386 1171	No	2.91	80.16	1.55	41.75
	cwi 566 3984	No	13.32	106.25	3.95	54.08
	vasy 574 13561	No	27.26	272.05	8.17	188.69
	vasy 720 390	No	0.86	31.45	0.76	17.45
	vasy 1112 5290	No	10.49	89.86	5.24	97.93
	cwi 2165 8723	Yes	1.87	61.94	2.15	48.80
	cwi 2416 17605	Yes	3.10	87.61	3.44	76.30
	vasy 2581 11442	No	32.70	326.38	14.78	214.93
	vasy 4220 13944	No	43.93	423.03	24.71	330.85
	vasy 4338 15666	No	47.55	479.15	28.06	344.64
	vasy 6020 19353	Yes	3.23	100.24	3.57	106.43
	vasy 6120 11031	No	30.59	425.64	38.37	437.71
	cwi 7838 59101	Yes	11.34	250.68	11.58	236.09
	vasy 8082 42933	No	119.77	1123.85	106.49	908.29
	vasy 11026 24660	No	60.86	698.85	108.97	804.34
	vasy 12323 27667	No	68.50	793.83	134.44	898.61
	cwi 33949 165318	Yes	33.89	732.05	34.60	738.78

APPENDIX C. PROOF OF SOUNDNESS AND COM-PLETENESS OF SCTL

The soundness and completeness of SCTL are guaranteed by the finiteness of the Kripke model. In the soundness THE COMPUTER JOURNAL, Vol. ??, No. ??, ????

TABLE B . 7 .

 B7 Livelock detection in SCTLProV and CADP

	proof, Proposition 3.1 and 3.2 permit to transform finite
	structures into infinite ones, and in the completeness
	proof, Proposition 3.3 and 3.4 permit to transform infinite
	structures into finite ones. The detailed soundness and
	completeness proofs are given as follows.

THEOREM C.1 (Soundness). If φ is closed, and the sequent φ has a proof π in SCTL(M ), then M |= φ for the given Kripke model M .

  |=AX x (φ 1 )(s).• If the last rule of π is EX-R, then the proved sequent has the form EX x (φ 1 )(s). By induction hypothesis, for some s in Next(s), M |= (s /x)φ 1 , hence M |= EX x (φ 1 )(s).• If the last rule of π is AF-R 1 or AF-R 2 , then the proved sequent has the form AF x (φ 1 )(s). We associate a finite path-tree |π| to the proof π by induction in the following way.-If the proof π ends with the AF-R 1 rule with a subproof ρ of the sequent (s/x)φ 1 , then the pathtree contains a single node s.-If the proof π ends with the AF-R 2 rule, with subproofs π 1 , ..., π n of the sequent AF x (φ 1 )(s 1 ), ..., AF x (φ 1 )(s n ), respectively, then |π| is the path-tree s(|π 1 |, ..., |π n |).

1 )(s). By induction hypothesis, for each s in Next(s), M |= (s /x)φ 1 , hence M

https://github.com/sctlprov/sctlprov_code

http://ocaml.org/

http://www.ensiie.fr/ ˜guillaume.burel/ blackandwhite_iProverModulo.html.en

http://lcs.ios.ac.cn/ ˜zwh/verds/index.html

http://nusmv.fbk.eu/

https://nuxmv.fbk.eu/

http://cadp.inria.fr/

Intuitively, we use the left hand side of the sequent to store visited states for co-inductive modalities.

With a little abuse of notation, we add AF x (φ)(s) into the context, instead of ¬AF x (φ)(s).

cpt( AF x (¬P(x))(a), t, f) * cpt(Γ AF x (¬P(x))(b), cpt(Γ AF x (¬P(x))(c), t, f), f) * cpt(Γ 1 AF x (¬P(x))(d), cpt(Γ AF x (¬P(x))(c), t, f), f) * cpt(Γ 2 AF x (¬P(x))(d), cpt(Γ AF x (¬P(x))(c), t, f), f) f

A more detailed explanation of the global variables in the proof search algorithm can be found in Appendix A.

cpt( EG x (P(x))(s 0 ), t, f) * cpt(Γ 0 EG x (P(x))(s 1,1 ), t, cpt(Γ 0 EG x (P(x))(s 2,0 ), t, f)) * cpt(Γ 1,1 EG x (P(x))(s 1,2 ), t, cpt(Γ 0 EG x (P(x))(s 2,0 ), t, f)) * . . . * cpt(Γ 1,n-1 EG x (P(x))(s 1,n ), t, cpt(Γ 0 EG x (P(x))(s 2,0 ), t, f)) * cpt(Γ 0 EG x (P(x))(s 2,0 ), t, f) * cpt(Γ 2,0 EG x (P(x))(s 1,1 ), t, cpt(Γ 2,0 EG x (P(x))(s 2,1 ), t, f)) * . . . * cpt(Γ 2,0 EG x (P(x))(s 2,1 ), t, f) * . . . * cpt(Γ 2,n-1 EG x (P(x))(s 2,n ), t, f) * cpt(Γ 2,n EG x (P(x))(s 2,n ), t, f) t

https://github.com/sctlprov/sctlprov_code

https://github.com/terminatorlxj/VMDV

http://lcs.ios.ac.cn/ ˜zwh/verds/verds_code/ bp12.rar

http://cadp.inria.fr/resources/vlts/

http://cadp.inria.fr/

https://github.com/sctlprov/sctlprov_sats

Next(s), and Γ = Γ ∪ {EU x,y (φ 1 , φ 2 )(s)}, then cpt(Γ EU x,y (φ 1 , φ 2 )(s), c 1 , c 2 ) rewrites to c 1 before it rewrites to c 2 implies that one of the following two cases holds.1. cpt(Γ EU x,y (φ 1 , φ 2 )(s), c 1 , c 2 ) * cpt( (s/y)φ 2 , c 1 , cpt( (s/x)φ 1 , cpt( Γ EU x,y (φ 1 , φ 2 )(s 1 ), c 1 , cpt(...cpt( Γ EU x,y (φ 1 , φ 2 )(s n ), c 1 , c 2 )...)), c 2 )) * c 1 ; 2. cpt(Γ EU x,y (φ 1 , φ 2 )(s), c 1 , c 2 ) * cpt( (s/y)φ 2 , c 1 , cpt( (s/x)φ 1 , cpt( Γ EU x,y (φ 1 , φ 2 )(s 1 ), c 1 , cpt(...cpt( Γ EU x,y (φ 1 , φ 2 )(s n ), c 1 , c 2 )...)), c 2 )) *

In the rules of the proof system, the context of an EU sequent is always empty. However, to make the proof easier to follow, the contexts of EU sequents are kept. The contexts of EU sequents does not break the structure of the proof tree since this kind of contexts are not examined in the proof tree. The purpose of introducing contexts for the EU case is explained in Section 4.1.1.

ACKNOWLEDGEMENTS

The authors would like to thank all anonymous referees for their valuable comments which improve significantly the present paper. The first author would like also to thank Ahmed Bouajjani and Wenhui Zhang for the beneficial discussions on model checking. This work was supported by the CAS-INRIA project VIP (GJHZ1844) and the NSFC-ANR project LOCALI (NSFC 61161130530 and ANR-11-IS02-00201).

In this section, we explain the pseudo code of our proof search algorithm in details.

First, let us define the notion of formula schema. For an SCTL(M ) formula φ with modality AF, EG, AR, or EU, a schema φ -of φ is defined by replacing the state constant in φ by . For instance, the schema of the formula EU x,y (φ 1 , φ 2 )(s) is EU x,y (φ 1 , φ 2 )( ), and the schema of the formula AF x (φ )(s ) is AF x (φ )( ). A formula schema can be viewed as a context of a state constant in an SCTL(M ) formula.

The pseudo code of the proof search algorithm is depicted in Figure A.1, in which the notations are listed as follows.

• ψ denotes the sequent to be proved in SCTL. • c denotes the CPT to be rewritten.

• pt and ce denote the proof tree and counterexample to be constructed during the proof search, respectively. • M t (resp. M f ) is used to store the set of visited states on which a sub-formula of ψ holds (resp. does not hold), and they are used to avoid visiting the same state repeatedly. Note that M t and M f are explained as hash tables. In fact, each of these two global variables remembers a set of states for each formula schema. Thus, a formula schema is a key, and a set of states is a value to these two hash tables. We denote, for instance, M t EG x (φ)( ) to the set of states S such that ∀s ∈ S, EG x (φ)(s) holds, and M f EG x (φ)( ) to the set of states S such that ∀s ∈ S, EG x (φ)(s) does not hold.

• visited is used to store temporally the visited states by sub-formula of ψ, starting with EU or AR (if any), and these states will be added into either M t or M f in later rewriting steps. Like M t and M f , visited can also be seen as a hash table. For instance, we denote visited EU x,y (φ 1 ,φ 2 )( ) to the set of visited states during the proof search of an EU formula. • We associate a set of actions A to each CPT c, written as c A . When rewriting a CPT c, each action in A needs to be performed. For instance, for a CPT c = cpt(Γ φ, c 1 , c 2 ), three sets of actions A 0 , A 1 , A 2 are associated to c, c 1 , c 2 , respectively. c A 0 is written as

). When rewriting c, the actions in A 0 need to be performed. The actions in A 1 cannot be performed until c rewrites to c 1 . When rewriting c 1 , the Appendix A. [START_REF] Baier | Principles of Model Checking[END_REF]

. ProveEG and ProveAF

The pseudo code for the ProveEG case is depicted in Figure A.6, where states(Γ) represents the set of states that appear in Γ. In this case, we let {s 1 , ..., s n } = Next(s), and Γ = Γ ∪ {EG x (φ 1 )(s)}. The pseudo code for this case is explained as follows.

• Line 3 -4: If EG x (φ 1 )(s) does not hold, then just rewrite c to c 2 .

then rewrite c to c 1 , and every formula in Γ holds and its corresponding state is thus added into M t EG x (φ 1 )( ) . • Line 15 -16: The CPT c is constructed with the following information integrated into c .

1. If c rewrites to the outer c 2 in the future steps, then (s/x)φ 1 is not provable, and thus (s/x)φ 1 will be added as the evidence of negating Γ EG x (φ 1 )(s) in the counterexample (Line 9). At the same time, since Γ EG x (φ 1 )(s) is not provable, we add s into M f EG x (φ 1 )( ) (Line 13). 2. If c rewrites to the inner c 2 , then Γ EG x (φ 1 )(s 1 ), ..., Γ EG x (φ 1 )(s n ) are all added as the evidence of negating Γ EG x (φ 1 )(s) in the counterexample (Line 10). At the same time, since Γ EG x (φ 1 )(s) is not provable, we add s into M f EG x (φ 1 )( ) (Line 14). 3. If c rewrites to the ith c 1 , then both (s/x)φ 1 and Γ EG x (φ 1 )(s i ) are provable, and thus should be added as the evidence of proving Γ EG x (φ 1 )(s) in the proof tree (Line 11 -12).

• Line 17: Rewrite c to c .

1: /* For notation purpose, here we refer "k" to EG x (φ 1 )( ) and 2: "k(s)" to EG x (φ 1 )(s).*/

∀i ∈ {1, ..., n}, let 12: [START_REF] Emerson | Using branching time temporal logic to synthesize synchronization skeletons[END_REF] shows the details of ProveAF, which is the dual case of ProveEG.

1: /* For notation purpose, here we refer "k" to AF x (φ 1 )( ) and 2: "k(s)" to AF x (φ 1 )(s).*/ 3: if s ∈ M t k then 4:

∀i ∈ {1, ..., n}, let 12:

A 10 := A 10 ∪ {M t k := M t k ∪ {s}} 14:

. ProveEU and ProveAR

The EU case is more complex than the EG case. The reason is that the EG case terminates when a cycle is detected, while the EU case does not terminate after detecting a number of cycles, until a non-cycle that satisfies a certain condition is detected. In this case, we let {s 1 , ..., s n } = Next(s), Γ = Γ ∪ {EU x,y (φ 1 , φ 2 )(s)}, and use reachable(S) to denote the set of visited states that can reach some state in S, where S represents the set of states in a finite path. Each state in reachable(S) is either in S, or in a finite path whose last state lies in a cycle overlapping with S at some state. The set reachable(S) can be calculated on-the-fly by remembering all visited cycles and merges and then selecting all states in each merge whose last state either lies in S, or lies in a cycle overlapping with S at some state.

The pseudo code for ProveEU (Figure A.8) is explained as follows.

• Line 3 -6: If EU x,y (φ 1 , φ 2 )(s) holds, then just rewrite c to c 1 . At the same time, all states in reachable(states(Γ)) are added into M t EU x,y (φ 1 ,φ 2 )( ) and removed from M f EU x,y (φ 1 ,φ 2 )( ) . • Line 7 -9: If s has been visited, then just rewrite c to c 2 . At the same time, all states in states(Γ) are added into M f EU x,y (φ 1 ,φ 2 )( ) to avoid being visited again. • Line 26 -27: The CPT c is constructed with the following information integrated into c .

1. If c rewrites to the first c 1 , then (s/y)φ 2 should be added to the proof tree as the evidence of proving Γ EU x,y (φ 1 , φ 2 )(s) (Line 12). At the same time, if (s/y)φ 2 holds, then for each state s that can reach s, EU x,y (φ 1 , φ 2 )(s ) also holds, so we add reachable(states(Γ) ∪ {s}) into M t EU x,y (φ 1 ,φ 2 )( ) , and remove all states in reachable(states

∀i ∈ {1, ..., n} , let 20:

visited k := {s} 23: else 24:

We show the detailed experimental data for benchmark #1, #2, #3, and #4 as follows.

Appendix B.

∀i ∈ {1, ..., n}, let 20:

visited k := {s} 23: else 24:

NuXMV: NuSMV and NuXMV solve all the 2880 test cases, while SCTLProV solves 2870 (99.7%) test cases.

Let us now turn to the efficiency. SCTLProV is much faster than the four other tools (Table B Given an LTS L = s 0 , S, Act, → where s 0 ∈ S is the initial state, S is a finite set of states, Act is a finite set of actions, and →⊆ S × Act × S is the transition relation. L is translated into a Kripke model M = s 0 , S , -→, P by performing the following transformation, where S = (S ∪ {s d }) × (Act ∪ {.}), s 0 ∈ S , -→⊆ S × S , and P = {P, Q}. or s is also a label of a node on the branch from the root of |π| to this leaf. Using Proposition 3.2, there exists a possibly infinite path-tree T such that for each node s of T , M |= (s /y)φ 2 , and for each leaf s of T , M |= (s /x)φ 1 . Thus, M |= AR x,y (φ 1 , φ 2 )(s).

• If the last rule of π is EU-R 1 or EU-R 2 , then the proved sequent has the form EU x,y (φ 1 , φ 2 )(s). We associate a finite sequence |π| to the proof π by induction in the following way.

-

If the proof π ends with the EU-R 1 rule with a sub-proof ρ of the sequent (s/y)φ 2 , then the sequence contains a single element s.

-

If the proof π ends with the EU-R 2 rule, with subproofs ρ and π 1 of the sequents (s/x)φ 1 and EU x,y (φ 1 , φ 2 )(s ), respectively, then |π| is the sequence s|π 1 |.

The sequence |π| = s 0 , ..., s n is such that s 0 = s; for each i between 0 and n -1, s i -→ s i+1 ; for each i between 0 and n -1, the sequent (s i /x)φ 1 has a proof smaller than π; and the sequent (s n /y)φ 2 has a proof smaller than π. By induction hypothesis, for each i between 0 and n -1, M |= (s i /x)φ 1 and M |= (s n /y)φ 2 . Hence, M |= EU x,y (φ 1 , φ 2 )(s).

• The last rule cannot be a merge rule. Proof. By induction over the size of φ.

• If φ = P(s 1 , ..., s n ), then as M |= P(s 1 , ..., s n ), the sequent P(s 1 , ..., s n ) is provable with the rule atom-R.

• If φ = ¬P(s 1 , ..., s n ), then as M |= ¬P(s 1 , ..., s n ), the sequent ¬P(s 1 , ..., s n ) is provable with the rule ¬-R.

• If φ = , then is provable with the rule -R.

By induction hypothesis, the sequents φ 1 and φ 2 are provable. Thus the sequent φ 1 ∧ φ 2 is provable with the ∧-R rule.

By induction hypothesis, the sequent φ 1 or φ 2 is provable and the sequent φ 1 ∨ φ 2 is provable with the ∨-R 1 or ∨-R 2 rule, respectively.

• If φ = AX x (φ 1 )(s), as M |= AX x (φ 1 )(s), for each state s in Next(s), we have M |= (s /x)φ 1 . By induction hypothesis, for each s in Next(s), the sequent (s /x)φ 1 is provable. Using these proofs and the AX-R rule, we build a proof of the sequent AX x (φ 1 )(s).

• If φ = EX x (φ 1 )(s), as M |= EX x (φ 1 )(s), there exists a state s in Next(s) such that M |= (s /x)φ 1 .

By induction hypothesis, the sequent (s /x)φ 1 is provable. With this proof and the EX-R rule, we build a proof of the sequent EX x (φ 1 )(s).

• If φ = AF x (φ 1 )(s), as M |= AF x (φ 1 )(s), there exists a finite path-tree T such that T has root s, for each internal node s , the children of this node are labeled by the elements of Next(s ), and for each leaf s , M |= (s /x)φ 1 . By induction hypothesis, for every leaf s , the sequent (s /x)φ 1 is provable. Then, to each subtree T of T , we associate a proof |T | of the sequent AF x (φ 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 built with the AF-R 1 rule from the proof of (a/x)φ 1 given by the induction hypothesis. This way, the proof |T | is a proof of the sequent AF x (φ 1 )(s).

• If φ = EG x (φ 1 )(s), as M |= EG x (φ 1 )(s), there exists a path s 0 , s 1 , ... such that s 0 = s and for all i, M |= (s i /x)φ 1 . By induction hypothesis, all the sequents (s i /x)φ 1 are provable. Using Proposition 3.3, there exists a finite sequence T = s 0 , ..., s n such that for all i, s i -→ s i+1 , the sequent (s i /x)φ 1 is provable and s n is some s p for p < n. We associate a proof |s i , ..., s n | of the sequent EG x (φ 1 )(s 0 ), . . . , EG x (φ 1 )(s i-1 ) EG x (φ 1 )(s i ) to each suffix of T by induction as follows.

-

The proof |s n | is built with the EG-merge rule. -If i ≤ n -1, then the proof |s i , ..., s n | is built with the EG-R rule from the proof of (s i /x)φ 1 given by the induction hypothesis and the proof |s i+1 , ..., s n | of the sequent EG x (φ 1 )(s 0 ), ..., EG x (φ 1 )(s i ) EG x (φ 1 )(s i+1 ).

This way, the proof |s 0 , ..., s n | is a proof of the sequent EG x (φ 1 )(s).

, there exists a possibly infinite path-tree such that the root of this tree is s, for each node s , M |= (s /y)φ 2 and for each leaf s , M |= (s /x)φ 1 . By induction hypothesis, for each node s of the path-tree, the sequent (s /y)φ 2 is provable and for each leaf s of the path-tree, the sequent (s /x)φ 1 is provable. Using Proposition 3.4, there exists a finite path-tree T such that for each node s of T , the sequent (s /y)φ 2 is provable, and for each leaf s , either the sequent (s /x)φ 1 is provable or s is also a label of a node on the branch from the root of T to this leaf. Then, to each sub-tree T of T , we associate a proof |T | of the sequent AR x,y (φ 1 , φ 2 )(s 1 ), ..., AR x,y (φ 1 , φ 2 )(s m ) AR x,y (φ 1 , φ 2 )(s ) where s is the root of T and s 1 , ..., s m is the sequence of nodes in T from the root of T to the root of T .

-If T contains a single node s , and the sequent (s /x)φ 1 is provable then the proof |T | is built with the AR-R 1 rule from the proofs of (s /x)φ 1 and (s /y)φ 2 given by the induction hypothesis.

- This way, the proof |T | is a proof of the sequent AR x,y (φ 1 , φ 2 )(s).

there exists a finite sequence T = s 0 , ..., s n such that M |= (s n /y)φ 2 and for all i between 0 and n -1, M |= (s i /x)φ 1 . By induction hypothesis, the sequent (s n /y)φ 2 is provable and for all i between 0 and n -1, the sequent (s i /x)φ 1 is provable. We associate a proof |s i , ..., s n | of the sequent EU x,y (φ 1 , φ 2 )(s i ) to each suffix of T by induction as follows.

-

The proof |s n | is built with the EG-R 1 rule from the proof of (s n /y)φ 2 given by the induction hypothesis.

-

If i ≤ n -1, then the proof |s i , ..., s n | is built with the EG-R 2 rule from the proof of (s i /x)φ 1 given by the induction hypothesis and the proof |s i+1 , ..., s n | of the sequent EU x,y (φ 1 , φ 2 )(s i+1 ).

This way, the proof |s 0 , ..., s n | is a proof of the sequent EU x,y (φ 1 , φ 2 )(s).

APPENDIX D. PROOF OF THE CORRECTNESS OF THE PROOF SEARCH METHOD

PROPOSITION D.1. Given a closed formula φ, cpt( φ, t, f) * t iff φ is provable.

Proof. The proof is split into two cases: given a closed formula φ, ⇒ : cpt( φ, t, f) * t implies that φ is provable; ⇐ : φ is provable implies that cpt( φ, t, f) * t.

For the "⇒" case, we prove a generalized proposition: for any two different CPTs c 1 , c 2 and a sequent Γ φ where φ is a closed formula, cpt(Γ φ, c 1 , c 2 ) rewrites to c 1 before it rewrites to c 2 implies that Γ φ is provable (i.e., a proof tree T of Γ φ can be constructed). The proof of this proposition is by induction on the weight (Definition 4.3) of Γ φ.

Before we prove the "⇒" case, it should be noted that for a CPT cpt(Γ φ, c 1 , c 2 ) where c 1 = c 2 , and φ is a closed formula, if cpt(Γ φ, c 1 , c 2 ) rewrites to c 1 before it rewrites to c 2 , then cpt(Γ φ, c 1 , c 2 ) rewrites to c 1 before it rewrites to c 2 for any two different CPTs c 1 and c 2 . This is because in the rewriting steps from cpt(Γ φ, c 1 , c 2 ) to c 1 , neither c 1 nor c 2 is examined until c 1 is to be rewritten. Thus, we can safely replace c 1 by c 1 , and c 2 by c 2 in the rewriting steps from cpt(Γ φ, c 1 , c 2 ) to c 1 , and obtain the rewriting steps from cpt(Γ φ, c 1 , c 2 ) to c 1 . Analogously, if cpt(Γ φ, c 1 , c 2 ) rewrites to c 2 before it rewrites to c 1 , then cpt(Γ φ, c 1 , c 2 ) rewrites to c 2 before it rewrites to c 1 for any two different CPTs c 1 and c 2 . These assertions are used in the proof of the "⇒" case. Now the proof of the "⇒" case is presented as follows.

• If Γ φ = , trivial. • If Γ φ = P(s 1 , ..., s n ) where P(s 1 , ..., s n ) is an atomic formula, then the only way that cpt( P(s 1 , ..., s n ), c 1 , c 2 ) rewrites to c 1 before it rewrites to c 2 is that cpt( P(s 1 , ..., s n ), c 1 , c 2 ) c 1 , in which case s 1 , ..., s n ∈ P. Then, it is sufficient to take the following proof tree as T .

) where P(s 1 , ..., s n ) is an atomic formula, then the only way that cpt( ¬P(s 1 , ..., s n ), c 1 , c 2 ) rewrites to c 1 before it rewrites to c 2 is that cpt( ¬P(s 1 , ..., s n ), c 1 , c 2 ) c 1 , in which case s 1 , ..., s n / ∈ P. Then, it is sufficient to take the following proof tree as T . ¬P(s 1 , ..., s n ) ¬-R

• If Γ φ = φ 1 ∧ φ 2 , then the only way that cpt( φ 1 ∧ φ 2 , c 1 , c 2 ) rewrites to c 1 before it rewrites to c 2 is that cpt( φ 1 ∧ φ 2 , c 1 , c 2 ) cpt( φ 1 , cpt( φ 2 , c 1 , c 2 ), c 2 ) * cpt( φ 2 , c 1 , c 2 ) * c 1 , then according to the induction hypothesis, both φ 1 and φ 2 are provable. This is because otherwise, if either φ 1 or φ 2 is not provable, then according to the induction hypothesis, cpt( φ 1 , cpt( φ 2 , c 1 , c 2 ), c 2 ) will rewrite to c 2 before it rewrites to c 1 . Suppose T 1 and T 2 are the proof trees constructed for φ 1 and φ 2 , respectively, then it is sufficient to take the following proof tree as T .

then there are two ways that cpt( φ 1 ∨ φ 2 , c 1 , c 2 ) rewrites to c 1 before it rewrites to c 2 :

cpt( φ 1 , c 1 , cpt( φ 2 , c 1 , c 2 )), and cpt( φ 1 , c 1 , cpt( φ 2 , c 1 , c 2 )) rewrites to c 1 before it rewrites to cpt( φ 2 , c 1 , c 2 ). In this case, according to the induction hypothesis, φ 1 is provable. Suppose T 1 is the proof tree constructed for φ 1 , cpt(Γ EU x,y (φ 1 , φ 2 )(s 1 ), c 1 , cpt(...cpt( Γ EU x,y (φ 1 , φ 2 )(s n ), c 1 , c 2 )...)) * cpt(Γ EU x,y (φ 1 , φ 2 )(s i ), c 1 , cpt(...cpt( Γ EU x,y (φ 1 , φ 2 )(s n ), c 1 , c 2 )...)) * c 1 where 1 ≤ i ≤ n.

If case 1 holds, then by induction hypothesis, (s/y)φ 2 is provable. Suppose T is the constructed proof tree of (s/y)φ 2 , then it is sufficient to take the following proof tree as T . 26 T Γ EU x,y (φ 1 , φ 2 )(s)

EU-R 1

If case 2 holds, then by induction hypothesis, both (s/x)φ 1 and Γ EU x,y (φ 1 , φ 2 )(s i ) are provable. Let T 1 and T 2 be the constructed proof trees of (s/x)φ 1 and Γ EU x,y (φ 1 , φ 2 )(s i ), respectively, and it is sufficient to take the following proof tree as T .

• If Γ φ = Γ AR x,y (φ 1 , φ 2 )(s), as the dual case of EU, the analysis for the AR case is analogous to that of the EU case.

For the "⇐" case, we also prove a generalized proposition: for two different CPTs c 1 and c 2 , and a closed formula φ,

• if φ is an inductive formula, then φ is provable implies that cpt( φ, c 1 , c 2 ) rewrites to c 1 before it rewrites to c 2 ;