Automatic Verification of Partial Correctness of Golog Programs

1 Introduction

Building autonomous agents that follow human's high-level guiding instructions, and accordingly figure out a concrete plan to carry out, is always a challenge of artificial intelligence. One possible solution to achieve this goal is to use high-level programming language, such as Golog [Levesque et al., 1997], which is a logic programming language based on the situation calculus [Reiter, 2001]. Provided with domain descriptions and possibly nondeterministic instructions, a Golog interpreter is able to generate a sequence of concrete actions, so programmers are released from the burden of specifying every single detail.

When Golog programs are used to control agents' behaviour in a high-level manner, their partial correctness naturally becomes an important concern. Roughly speaking, partial correctness states that if some properties hold at the beginning, then some other properties must hold after the program is executed. Liu [2002] proposed a Hoare-style proof system for partial correctness of Golog programs. However, she didn't address the automatic verification issue.

Partial correctness is also a central topic in the software engineering community. There have been two important approaches for verification: static analysis and dynamic analysis. Static analysis tries to verify programs by analyzing the source code without actually executing them. Usually verification by static analysis is guaranteed to be sound, but at the cost of inefficiency [Flanagan and Qadeer, 2002; Pasareanu and Visser, 2004]. On the contrary, dynamic analysis tries to discover faults by running the program with adequate test cases. Generally this approach leads to faster algorithms and implementations, but there is no guarantee that the program is correct even if all test cases behave as expected [Nguyen et al., 2012].

When we human try to prove or disprove a mathematical assertion, we are using the static and dynamic analysis unconsciously, and integrate them in a sophistical way. We first attempt to prove it by following some routines and heuristics that were learned before; if a proof is not found, we may look for some examples to illustrate which step during the attempted proof goes wrong, and then fix it and continue the proof. If lucky we may also find a counterexample and thus disprove the assertion. One may go back and forth between reasoning and testing, until a proof or a disproof is achieved. Based on this observation, in this paper we propose a method that combines the static and dynamic analysis, which tries to imitate the reasoning process of human.

We introduce the notion of extended regression, which belongs to the static analysis paradigm. By extended regression one can regress a formula wrt a Golog program. It has a similar property as regression in the situation calculus: a formula holds after executing a program, if it's extended regression holds before the execution. Thus we reduce partial correctness of Golog programs to first-order entailment problems.

When extended regression is applied to a loop statement, we need to discover an appropriate loop invariant. Recently, we proposed a sound but incomplete method for automatic verification and discovery of state constraints in the situation calculus [Li et al., 2013]. The basic idea presented in this paper is similar to the previous work: we start with a simple formula, and then strengthen it iteratively until it becomes a loop invariant. During this process, formulas used for strengthening are generated by heuristic methods. It turns out that the method for inferring loop invariants can also be adapted to verify state constraints.

The heuristic functions generate a set of heuristic candidates. When deciding which of the candidates should be selected for strengthening, we use small models to filter out the too strong ones, which is the dynamic analysis component in our method. Specifically, a set of initial small models are provided by the user, which can be viewed as several test inputs. We progress these initial small models wrt the program, associating each loop with a set of small models. These associated small models can be regarded as a set of possible program states. Later when heuristic functions generate a set of heuristic candidates, we select the one as strong as possible provided it is satisfied by the associated small models.

2 Preliminaries

2.1 The Situation Calculus and Golog

The situation calculus [Reiter, 2001] is a many-sorted first-order language for representing dynamic worlds. There are three disjoint sorts: action for actions, situation for situations, and object for everything else. A situation calculus language has the following components: a constant S0 denoting the initial situation; a binary function do(a, s) denoting the successor situation to s resulting from performing action a; a binary predicate s ⊑ s′ meaning that situation s is a subhistory of situation s′ ; a binary predicate Poss(a, s) meaning that action a is possible in situation s; a countable set of action functions, e.g., move(x, y); and a countable set of relational fluents, i.e., predicates taking a situation term as their last argument, e.g., ontable(x, s).

Often, we need to restrict our attention to formulas that do not refer to any situations other than a particular one τ, and we call such formulas uniform in τ. We use φ(τ) to denote that φ is uniform in τ. We call a uniform formula φ with all situation arguments eliminated a situation-suppressed formula, and use φ[s] to denote the uniform formula with all situation arguments restored with term s. A situation s is executable if it is possible to perform the actions in s one by one: Exec(s) .= ∀a, s′ .do(a, s′ ) ⊑ s ⊃ Poss(a, s′ ).

In the situation calculus, a particular domain of application is specified by a basic action theory (BAT) of the form:

1. Σ is the set of the foundational axioms for situations.
2. Dap contains a single precondition axiom of the form Poss(a, s) ≡ Π(a, s), where Π(a, s) is uniform in s.
3. Dss is a set of successor state axioms (SSAs), one for each fluent F , of the form F (⃗x, do(a, s)) ≡ ΦF (⃗x, a, s), where ΦF (⃗x, a, s) is uniform in s.
4. Duna is the set of unique names axioms for actions.
5. DS0 , the initial KB, is a set of sentences uniform in S0.

The formal semantics of Golog is specified by an abbreviation Do(δ, s, s′ ), which is inductively defined as follows:

1. Primitive actions: For any action term α, Do(α, s, s′ ) .= Poss(α, s) ∧ s′ = do(α, s).
2. Test actions: For any situation-suppressed formula φ, Do(φ?, s, s′ ) .= φ[s] ∧ s = s′ .
3. Sequence: Do(δ1; δ2, s, s′ ) .= ∃s′′ .Do(δ1, s, s′′ ) ∧Do(δ2, s′′ , s′ ).
4. Nondeterministic choice of two actions: Do(δ1|δ2, s, s′ ) .=Do(δ1, s, s′ ) ∨Do(δ2, s, s′ ).
5. Nondeterministic choice of action arguments: Do((πx)δ(x), s, s′ ) .= (∃x)Do(δ(x), s, s′ ).
6. Nondeterministic iteration:

Conditionals and loops are defined as abbreviations:

In this paper we consider programs with while statements, but without nondeterministic iterations appearing alone.

2.2 State Invariants and State Constraints

We now formally define state constraints and state invariants. We use |= to denote entailment in the situation calculus, and use |=FOL to denote classic first-order entailment. We follow the definition of state constraints in [Reiter, 2001]:

Definition 1. Given a BAT D and a formula φ(s), φ(s) is a state constraint for D if D |= ∀s.Exec(s) ⊃ φ(s).

State constraints are formulas which hold in all executable situations. We use DSC to denote a set of verified state constraints, and abuse DSC as the conjunction of its elements.

State invariants are formulas that if true in a situation, will be true in all successor situations. Verifying state invariants is a first-order reasoning task.

Definition 2. Let DSC be a set of verified state constraints. A formula φ(s) is a state invariant for D wrt DSC if

The following result shows that we can verify a constraint by proving that it is an invariant.

Proposition 1. If DS0 |=FOL ϕ(S0), and ϕ(s) is an invariant wrt DSC, then ϕ(s) is a constraint.

2.3 Regression andModel Progression

There are two important computational mechanisms for reasoning about actions and their effects in the situation calculus, namely regression and progression.

Here we define a one-step regression operator and state a simple form of the regression theorem [Reiter, 2001].

Definition 3. We use RD[φ] to denote the formula obtained from φ by replacing each fluent atom F(⃗t, do(α, σ)) with ΦF (⃗t, α, σ) and each precondition atom Poss(α, σ) with Π(α, σ), and further simplifying the result by using Duna.

Intuitively, the notion of progression is used to update the current world state after an action is executed. The progression of a theory is generally not first-order definable [Lin and Reiter, 1997]. In this paper, progression refers to the progression of models. We use progS [M, α] to denote the new model generated by updating model M according to action α.

Under the close world assumption, a model can be represented by a set of ground atoms, which we call a small model.

3 Theoretical Foundations

3.1 Partial Correctness and Extended Regression

We begin with a formal definition of Hoare triple and partial correctness in the context of Golog programs.

Definition 4. A Hoare triple is of the form {P}δ{Q}, where P and Q are situation-suppressed formulas, and δ is a Golog program. A Hoare triple {P}δ{Q} is said to be partially correct wrt D if D |= ∀s, s′ .P [s] ∧ Do(δ, s, s′ ) ⊃ Q[s′ ].

Next we present the notion of extended regression, which plays a significant role throughout this paper.

Definition 5. Given D and DSC, the extended regression of formula φ(s) wrt program δ, denoted as ˆRD[φ(s), δ], is defined as follows:

• ˆRD[φ(s), α] =RD(Poss(α, s) ⊃ φ(do(α, s))).
• ˆRD[φ(s), ψ?] = ψ[s] ⊃ φ(s).
• ˆRD[φ(s), δ1; δ2] = ˆRD[ ˆRD[φ(s), δ2], δ1].
• ˆRD[φ(s), δ1|δ2] = ˆRD[φ(s), δ1] ∧ ˆRD[φ(s), δ2].
• ˆRD[φ(s), (πx)δ(x)] = (∀x) ˆRD[φ(s), δ(x)].
• ˆRD[φ(s),while ϕ do δ od] is a formula (denoted as η(s)) satisfying the following two conditions:
• |=FOL ∀s.η(s) ∧ϕ[s] ∧DSC ⊃ ˆRD[η(s), δ].
• |=FOL ∀s.η(s) ∧DSC ⊃ φ(s) ∨ϕ[s].

Intuitively, in the definition of loop statement the first condition ensures the regression is a loop invariant, and the second condition guarantees this invariant is strong enough to entail the formula being regressed when the loop ends.

In the situation calculus, a formula holds after a sequence of actions are performed if and only if its regression can be entailed by the initial knowledge base. By structural induction we obtain a similar property for the extended regression operator, that is, a formula holds after the program is executed, if its extended regression holds before the execution.

Theorem 2. Let φ(s) be a formula, δ be a Golog program and D as before, we have

This furnishes us with a method for proving partial correctness by extended regression:

Corollary 1. A Hoare triple {P}δ{Q} is partially correct wrt D and DSC, if |=FOL ∀s.P[s] ∧DSC ⊃ ˆRD[Q[s], δ].

3.2 Heuristics for Finding Loop Invariants

The definition of extended regression is not specific about how to obtain a proper formula satisfying the two conditions of a loop statement. For the purpose of a concrete algorithm, we next discuss the weakest extended regression and how it inspires us in the heuristic approach.

Definition 6. The weakest extended regression of formula φ(s) wrt program δ, denoted as ˆWD[φ(s), δ], is the same as extended regression except for the case of loop statement.

• F(s)0 = φ(s)∨ϕ[s], F(s)i+1 = ¬ϕ[s]∨ ˆWD[F(s)i , δ]. ˆWD[φ(s), while ϕ do δ od] = ∧Ni=0 F (s)i , where N is a natural number s.t. F(s)N is equivalent to F(s)N+1 .

As the next proposition shows, ˆWD[φ(s), δ] is sufficient and necessary for φ(s) to be true after the execution of δ. The proof is another application of structural induction on δ.

Proposition 2. Let φ(s) be a formula, δ be a Golog program and D as before, we have

Weakest extended regression can be viewed as a process of strengthening. The process starts with φ(s) ∨ ϕ[s], and in the i-th step we strengthen it with F(s)i . If the process reaches a fixpoint, we obtain the weakest loop invariant. However, the fixpoint does not always exist, and even if it exists the strengthening process may be too slow to be practical. We are inspired to use a stronger formula to strengthen during each step, by which the convergence to fixpoint could be accelerated.

In what follows we identify three kinds of simple but useful heuristics. Each heuristics generates a set of heuristic candidates ∆, and the corresponding heuristic function returns one of them. It is guaranteed that every heuristic candidate in ∆ is stronger than or equivalent to its original formula. Every formula can be written in the form of ∃∗ ξ0(s) ∨ ∀∗ ξ1(s), where ξ0(s) and ξ1(s) may have other quantifiers.

Sub-Disjunction Heuristics

For formula ∃∗ ξ0(s) ∨∀∗ ξ1(s), the heuristic candidate set is: ∆SD(∃∗ ξ0(s) ∨ ∀∗ ξ1(s)) = {∃∗ ξ ′0 (s) ∨ ∀∗ ξ ′1 (s)|

Unification Heuristics

Every formula in ∆Uni((∃⃗x)ξ0(⃗x, s) ∨ (∀⃗y)ξ1(⃗y, s)) is obtained by the following steps:

1. Rename ⃗x, ⃗y to ⃗u, ⃗v such that ⃗u and ⃗v share no variables.
2. Choose n distinct variables ⃗c ∈ ⃗u, and n (unnecessarily distinct) variables ⃗ d ∈ ⃗v, let ⃗u′ = ⃗u\⃗c.
3. Obtain ξ ′0 (⃗u′ , ⃗ d, s) by replacing ⃗c with ⃗ d in ξ0(⃗u, s).
4. Let ∀⃗v∃⃗u′ .ξ ′0 (⃗u′ , ⃗ d, s) ∨ ξ1(⃗v, s) be a formula in ∆Uni.

Constant Heuristics

Let C be the set of all constants used in the Hoare triple. ∆Con((∃⃗x)ξ0(⃗x, s) ∨ ∀∗ ξ1(s)) is a set of formulas generated by replacing some variables in ⃗x with ⃗c ∈ C, or by changing some constants in ξ1(s) to universally quantified variables.

There is a dilemma when deciding which formula should our heuristic function return from the candidate set ∆. If the formula used for strengthening is too strong, we may end up with a too strong loop invariant. On the other hand, if the formula is too weak, the strengthening process may be too slow, just as the weakest extended regression. We solve this dilemma by using small models to filter out the too strong candidates. Among all the heuristic candidates we select the one as strong as possible provided it is satisfied by the associated small models. This is the topic of the next subsection.

3.3 Progression of Small Models

We begin with a definition of the progression operator.

Recall that a small model M is represented by a set of ground atoms. Given a finite constant set D, we use M[s] to denote the unique model such that only those atoms in M (with situation s restored) are satisfied.

Definition 7. We assume the ground terms are all constants from a finite set D. Given a small model M and a program δ, the progression of M wrt δ, denoted as prog[M, δ], results in a set of small models:

• prog[M, α] = 1. ∅ if M[s] ̸|= Poss(α, s). 2. {progS [M, α]} if M[s] |= Poss(α, s).
• prog[M, ψ?] = 1. ∅ if M[s] ̸|= ψ[s]. 2. {M} if M[s] |= ψ[s].
• prog[M, δ1; δ2] = prog[prog[M, δ1], δ2].
• prog[M, δ1|δ2] = prog[M, δ1] ∪ prog[M, δ2].
• prog[M, (πx)δ(x)] = ⋃{prog[M, δ(c)]|c ∈ D}.
• prog[M, δ∗ ] = ⋃n≥0 prog[M, δn ], where δn is an abbreviation of jointing n copies of δ sequentially.

When progressing wrt a loop the computation may never stop. In practice we preset a constant K, and let prog[M, δ∗ ] = ⋃Kn=0 prog[M, δn ].

The first usage of the small models is to prove a Hoare triple is not partially correct, while the extended regression can only be used to prove the positive result.

Theorem 3. If a Hoare triple {P}δ{Q} is partially correct, andM is a small model that M[s] |= P[s]∧DSC, then for all M ′ ∈ prog[M, δ] we have M ′ [s] |= Q[s].

Another important usage of our small models is to inform us that the regression "goes wrong" during the process. In particular, if some loop invariant is not satisfied by its associated small models, the final regression result will be too strong to be successfully verified. One step further, when generating a loop invariant, any heuristic candidate not satisfied by its associated small models should be discarded.

Proposition 3. If |=FOL ∀s.P[s] ∧ DSC ⊃ ˆRD[Q[s], δ1; δ2] and M[s] |= P[s] ∧DSC, then for all M ′ ∈ prog[M, δ1] we have M ′ [s] |= ˆRD[Q[s], δ2].

4 Algorithms

In this section we introduce three algorithms in detail: the top-level main algorithm, the loop invariant inferring algorithm and the state constraint discovering algorithm. The implementations for extended regression ˆRD and small model progression prog are basically the same as their definitions, and we omit the details. We assume that the underlying D, DSC and a finite set of constants D used for grounding are given, without providing them explicitly.

4.1 Main Algorithm

Algorithm 1 is the top-level algorithm of our system, which combines static and dynamic analysis. It tries to imitate the deduction process of a human reasoner: going back and forth between the processes of attempting a proof, and looking for a test case to illustrate why an attempted proof goes wrong.

Algorithm 1: veri(P, δ, Q,M)

Input: Hoare-triple {P}δ{Q}; M - initial small models that satisfy P and DSC. 1 Let asso be a function mapping each while construct in δ to a pair 〈true, ∅〉 2 〈M′ , asso〉 ← prog(M, δ, asso) 3 if ∃M ′ ∈M′ s.t. M ′ [s] ̸|= Q[s] then return no 4 counter ← 0 5 while counter <K1 do 6 counter ← counter + 1 7 〈reg(s), asso〉 ← ˆRD(Q[s], δ, asso) 8 if |=FOL ∀s.P[s] ∧DSC ⊃ reg(s) then return yes 9 while counter <K1 do 10 counter ← counter + 1 11 M0 ← genModel(DSC, P) 12 〈M′ , asso〉 ← prog(M0, δ, asso) 13 if ∃M ′ ∈M′ s.t. M ′ [s] ̸|= Q[s] then return no 14 if ∃ loop δl s.t. asso(δl) = 〈Invt(s),Mt〉 and ∃Mt ∈Mt s.t. Mt[s] ̸|= Invt(s) then break

At the beginning we initialize a function asso, mapping each while construct to a pair 〈inv,mod〉, where inv is the current candidate loop invariant and mod is the set of small models progressed to the beginning of the while construct. When we perform progression (Line 2, 12), the associated small models will be updated; similarly when we perform extended regression (Line 7), the associated candidate loop invariant will be updated.

In Line 2, we progress the set of initial small models wrt δ. Procedure prog returns a pair 〈M′ , asso〉, where M′ is the progression result and asso is the updated mapping function. If some model inM′ does not satisfy Q, we find a counterexample and the system returns no. Variable counter in Line 4 is used to guarantee the following loops terminate in finite steps. During each iteration of the outer loop, we first try to prove the positive result by extended regression in Line 7. When regressing a loop statement, the associated small models can be retrieved by asso function and be used to filter out too strong heuristic candidates.

If the entailment in Line 8 can be proved by the theorem prover, the system returns yes. Otherwise we enter a loop starting at Line 9. In Line 11, we generate a small model M0 that satisfies P[s] ∧ DSC and is different from those in M and any small model generated before. In procedure genModel, we ground DSC and P to a set of propositional formulas in CNF and call a SAT solver. Next, we progress M0 wrt δ. If some resulted small model does not satisfy Q, we find a counterexample and the system returns no as before. Then in Line 14, if there is a while construct δl such that one of its associated small models does not satisfy its associated loop invariant, we jump out of the loop and try the extended regression again. The inner loop guarantees that regression at Line 7 returns a new result each time.

Theorem 4. Algorithm veri(P, δ, Q,M) returns yes only if the Hoare triple {P}δ{Q} is partially correct, and returns no only if the Hoare triple is not partially correct.

4.2 Loop Invariant Inferring Algorithm

When regressing a loop statement, we call the infer procedure listed as Algorithm 2.

Algorithm 2: infer(φ(s), δl, asso)

Input: φ(s) - formula being regressed; δl - loop statement being regressed; asso as before 1 Let δl = while ϕ do δ od 2 η(s) ←φ(s) ∨ϕ[s]; counter ← 0 3 while counter <K2 do 4 counter ← counter + 1 5 〈reg(s), asso〉 ← ˆRD(η(s), δ, asso) 6 if |=FOL η(s) ∧ ϕ[s] ∧ DSC ⊃ reg(s) then 7 asso(δl).inv = η(s) 8 return 〈η(s), asso〉 9 Let reg(s) ≡ A1(s) ∧ ... ∧An(s), choose a Ai(s) s.t. ̸|=FOL η(s) ∧ ϕ[s] ∧ DSC ⊃ Ai(s) 10 Let Ai(s) ≡ ∃∗ ξ0(s) ∨ ∀∗ ξ1(s) 11 Transform ξ1(s) into conjunction C1(s)∧...∧Ct(s) 12 Choose Ci(s) s.t. ̸|=FOL η(s) ∧ ϕ[s] ∧ DSC ⊃ ∃∗ ξ0(s) ∨ ∀∗Ci(s) 13 can(s) ← heur(∃∗ ξ0(s) ∨ ∀∗Ci(s), asso(δl).mod) 14 η(s) ← η(s) ∧ can(s) 15 asso(δl).inv = false 16 return 〈false, asso〉

The candidate invariant η(s) is initialized as φ(s) ∨ ϕ[s]. In each step of the following iteration, we regress η(s) wrt the loop body. If the entailment in Line 6 can be proved, then η(s) is an appropriate invariant for δl. We update the asso function accordingly, and return 〈η(s), asso〉 as the result. If the entailment cannot be proven, we transform the regression result to a conjunction, choosing a conjunct Ai(s) which causes the failure of the entailment. If Ai(s) is not entailed, there must be some Ci(s) such that ∃∗ ξ0(s)∨∀∗Ci(s) cannot be entailed. In function heur we repeatedly apply the three heuristics in a greedy manner. Among all the possible candidates we select the one as strong as possible provided that it is satisfied by the associated small models asso(δl).mod. Finally we strengthen η(s) with the returned formula.

Proposition 4. Procedure infer(φ(s), δl, asso) returns 〈η(s), asso′ 〉, where η(s) is a formula that satisfies the definition of ˆRD[φ(s), δl].

4.3 State Constraints Discovering Algorithm

We can strengthen a formula φ(s) to a state invariant by regressing it wrt a constraint checking program δSC.

Definition 8. Suppose that the action functions in the application domain are a1( ⃗X1), ..., an( ⃗ Xn). The constraint checking program δSC is defined to be

Proposition 5. Loop invariant of δSC is also a state invariant.

When strengthening φ(s) to a loop invariant by regressing it wrt δSC, the only change of Algorithm 2 is that the initial formula to be strengthened is φ(s) instead of φ(s) ∨ true, which is trivial. By Propositions 1 and 5, if ˆRD[φ(s), δSC] is entailed by the initial KB then every conjunct of it, including φ(s), is a state constraint. In our implementation, the initial KB is represented by a set of small models. So checking the entailment could be done efficiently.

The constraint discovering algorithm follows the guessand-check paradigm as [Li et al., 2013] does, and we adopt the candidate enumerating method from [Rintanen, 2000]. Our candidate formulas are of the form (x1 ̸= x′1 ∧ ... ∧xn ̸= x′n ) ⊃ (L1 ∨ ... ∨ Lm), where Li are literals while xi and x′i are variables appearing as arguments of the literals. In practice we restrict n ≤ 1 and m ≤ 2. The candidate set Σ is initialized as Σ = {P1( ⃗ x1), ¬P1( ⃗ x1), P2( ⃗ x2), ...}, where P1( ⃗ x1), P2( ⃗ x2), . . . are all the predicates in the domain. If we could verify it is a state constraint, we move it along with the formulas used for strenghtening to DSC. Otherwise, we replace it with some weaker candidate constraints. There are three weakening operations for a given candidate constraint: adding a disjunct to the consequent, adding a conjunct x ̸= y to the antecedent and identifying two variables.

5 Experimental Results

We implemented the algorithms in SWI-Prolog. All experiments were conducted on a personal laptop equipped with 2.60 GHz CPU and 4.00GB RAM under Linux. We used E Prover [Schulz, 2013] as the underlying theorem prover, and MiniSat [E´en and S¨orensson, 2003] as the SAT solver.

Our system successfully verified 22 programs in 9 domains. Among them the logistics domain is from the AIPS'00 planning competition, and the other 8 domains are adapted from those used in [Hu, 2012]. For each domain, we discovered state constraints in advance, and used them as background knowledge in the later verifications.

5.1 ProgramVerification Examples

We use two examples to demonstrate the power of our system.

Green Domain Example

Figure 1 presents an example in the green domain, which resembles the blocks world domain. We introduce two new predicates green, collected and a new action collect. The goal is to collect all green blocks.

The program is composed of two sequential loops. First we unstack all towers onto the table, during which we collect all green blocks held by the robot. The second loop examines all the blocks remaining on the table and collect the green ones. The loop invariants for the two loops are listed as Inv1 and Inv2. To save space and to improve readability, we omit the initial formula being strengthened and manually simplify the final result. Our algorithm verified this program in 46.0s.

{handempty ∧ ∀x.green(x) ⊃ ontable(x) ∨ ∃y.on(x, y)}

while (∃x, y)on(x, y) do (πu, v)(unstack(u, v); if green(u) then collect(u) else putdown(u) fi) od ; while (∃x)(ontable(x) ∧ green(x)) do (πu)( if green(u) then pickup(u); collect(u) fi) od {∀x.green(x) ⊃ collected(x)} Inv1: ... ∧ ∀x.green(x) ⊃ ontable(x) ∨ collected(x) ∨ ∃y.on(x, y) Inv2: ... ∧ ∀x.green(x) ⊃ ontable(x) ∨ collected(x)

{holding(0) ∧ rob at(locA) ∧ ∀[o, obj].at(o, locB)} while ∃[x, obj].at(x, locB) do move(locA, locB); while ∃[y, obj].at(y, locB) ∧ ¬holding(2) do (π[y′ , obj])rob load(y′ , locB) od; move(locB, locA); while ∃[y, obj].gripped(y) do (π[y′ , obj])rob unload(y′ , locA) od od {∀[o, obj].at(o, locA)} Inv1: ... ∧ ∀[o, obj].at(o, locA) ∨ at(o, locB)

Figure 2: Example of the Gripper+ Domain

Gripper+ Domain Example

Figure 2 lists the verification of a program in the gripper+ domain. There is a robot with two hands, so it is able to hold two objects at the same time. We use holding(x) to denote that the robot is currently holding x objects, where x could be 0, 1 or 2. With the robot starting at locA, it tries to move all objects from locB to locA.

The program works as follows: As long as there are objects remaining at locB, the robot moves there, and loads objects until all its hands are occupied. Then it moves back to locA, unloads all objects that it gripes. Formula Inv1 is the loop invariant of the outer loop. The loop invariants of the two inner loops, denoted as Inv2 and Inv3, are identical ones. Our system succeeded in verifying the Hoare triple in 32.0s.

We hope to use the two examples above to demonstrate the following points: (1) our method is able to verify some interesting programs, and during the process succinct and comprehensible loop invariants are discovered; (2) the method can handle programs with sequential loops and nested loops in a uniform way; (3) the verification process usually terminates in a reasonable amount of time for such size of programs.

5.2 State Constraint Discovering Examples

When discovering state constraints we assume that type information is given. For instance, in predicate at(x, y) of the logistic domain, x is of type obj and y is of type loc. In this case we include ∀x, y.at(x, y) ⊃ obj(x) ∧ loc(y), ∀x.¬obj(x) ∨ ¬loc(x) in DSC beforehand.

Constraints discovered in the green domain cover the 12 ones of the blocks world domain presented in [Li et al.,

2013]. Since green domain introduces two new predicates green and collected, we discovered 5 more constraints:

{collected(x) ⊃ ¬clear(x), collected(x) ⊃ ¬on(x, y), collected(x) ⊃ ¬holding(x), collected(x) ⊃ ¬on(y, x),

Our constraint discovering algorithm is much faster than that in [Li et al., 2013]. We used 103.0s to discover all the 17 constraints in the green domain, while it took our previous system about 15min to discover the 12 ones in blocks world.

We discovered 3 constraints in the gripper+ domain:

{∀[o, obj][l, loc].gripped(o) ⊃ ¬at(o, l), ∀[l1, loc][l2, loc].rob at(l1) ∧ rob at(l2) ⊃ l1 = l2,

∀[x, num][y, num].holding(x) ∧ holding(y) ⊃ x = y}

5.3 Summary

We summarize the experimental results as Table 1. Under the Constraint column, #A is the number of all constraints we discovered, and T shows the total time cost. Under the Verification column, #A is the number of all Hoare triples we tested, and all of them were successfully verified. #N is the number of non-trivial verifications. We say a verification is trivial, if during the extended regression, every ˆRD[φ(s),while ϕ do δ od] returns φ(s) ∨ ϕ[s] as its loop invariant. T.avg and T.max are the average and maximal time costs of all verifications. Time costs are measured in seconds.

However, there are also a few programs in other domains that our system failed to verify. One reason is that the domains involve arithmetic, which calls for special heuristic functions; another reason is that our method suffers from the scalability problem, mostly due to the inefficiency of the underlying theorem prover.

6 Conclusion

In this paper we have proposed a sound but incomplete method for verifying partial correctness of Golog programs. The basic idea is to use extended regression to reduce the verification of a Hoare triple to a first-order entailment problem. When regressing a loop statement, we discover a proper loop invariant by strengthening a formula with heuristic methods and use small models to filter out too strong candidates.

We summarize our main contributions as follows. Firstly we have developed a practical method with solid theoretical foundations for verifying partial correctness of Golog programs. Secondly, we have proposed heuristic methods for discovering loop invariants, and identified three kinds of simple but useful heuristics. Thirdly, our algorithm combines static and dynamic analysis from the software engineering community. Fourthly, the method can also be adapted to discover state constraints. Lastly, we have implemented our algorithms, and experimental results show that our method can not only handle sequential and nested loops uniformly in a reasonable among of time, but also discover succinct and comprehensible loop invariants and state constraints.

There are at least three topics for future research. Firstly we would like to introduce heuristics for programs that involve arithmetic. The second challenge is to extend the method such that it could verify total correctness. Finally, we are interested in combining our approach with other successful methods, for example the predicate abstraction method in [Flanagan and Qadeer, 2002].

Acknowledgements

We thank Hector Levesque and Gerhard Lakemeyer for many helpful discussions about this paper. We are grateful to Yuxiao Hu for his valuable help with this work. Thanks also to the anonymous reviewers for useful comments. Yongmei Liu is also affiliated to the Guangdong Key Laboratory of Information Security Technology, Sun Yat-sen University, China. This work was partially supported by the Natural Science Foundation of China under Grant No. 61073053.