Reasoning about State Constraints in the Situation Calculus

1 Introduction

When an agent is working in a dynamic world, she needs to recognize and verify some laws of the world. Two kinds of laws widely investigated are state invariants and state constraints [Lin, 2004]. Roughly, state invariants are formulas that if true in a state, will be true in all successor states, while state constraints are formulas that hold in any reachable state. The key difference between them is that the first is a firstorder property while the second is a second-order property.

In planning, state constraints act as domain specific knowledge which reduces the search space greatly [Gerevini and Schubert, 1998]. Experiments show that they speed up planning drastically in some cases [Kautz and Selman, 1992; Gerevini and Schubert, 1998; Refanidis and Vlahavas, 2000]. State constraints can also be used to debug domain axiomatization. In C programs, we sometimes need to ensure that a pointer never moves out of an area, or a stack is never overflowed, so we are to verify whether they are state constraints.

The problems of discovering state constraints and invariants have been investigated in both the planning and reasoning about actions communities. The works from the planning community are more empirical. In the reasoning about action community, Lin [2004] developed a method for discovering state invariants in domains of unbounded size through exhaustive search in selected small domains. He did experiments in blocks world and logistics domains, and discovered a complete set of constraints in the second, that is, any illegal state must violate at least one of them. However, there is no soundness guarantee when his method is applied to non∀∗ -formulas. Kelly and Pearce [2010] proposed a method for computing whether a formula φ holds in all successor states of a given state, but the procedure does not necessarily halt since it is based on first-order entailment and fixpoint computation, and no implementation was reported.

In this paper, we propose a sound but incomplete method for automatic verification and discovery of ∀∗∃∗ state constraints for a class of action theories that include many planning benchmarks. Our method is formulated in the situation calculus, theoretically based on Skolemization and Herbrand Theorem, and implemented with SAT solvers.

Basically, we verify a state constraint by strengthening it with a sequence of formulas so that it becomes an invariant constraint, and the formulas used to strengthen it are called its joint constraints. So the problem becomes how to systematically obtain such joint constraints. We have developed a novel way to do so. Given a ∀∗ formula φ, assuming it holds in the initial state, we test if φ is a state invariant, using those previously verified constraints as the background information. If so we confirm that φ is a state constraint. Otherwise, we pick up a successor state s′ of state s such that φ(s) ⊃ φ(s′ ) is not entailed by the existing set of state constraints. We regress φ(s′ ) to get an equivalent formula ψ(s). For the class of action theories we consider, ψ(s) is also a ∀∗ formula. We convert ψ(s) into CNF, and we call each conjunct of it a derivant of φ. The derivants of φ not logically implied by φ have the nice property that if φ can be strengthened to become an invariant constraint, then they are joint constraints of φ. Next we obtain a derivant C not implied by φ, use it to strengthen φ, and continue this procedure with φ ∧ C. Besides, we also check if φ can be strengthened by some subset of C in order to obtain more intuitive and succinct joint constraints.

We did experiments in the blocks world, logistics and satellite domains, and the results showed that, almost all known constraints are verified in a reasonable time period, and meanwhile succinct and intuitive joint constraints are discovered.

2 Preliminaries

In this section, we introduce the background work of our paper, i.e., Herbrand Theorem and Skolemization, the situation calculus, state constraints and state invariants.

2.1 Herbrand Theorem

Herbrand Theorem reduces the satisfiability of a set of ∀∗ first-order sentences to that of a possibly infinite set of propositional formulas.

Theorem 2.1. Let L be a first-order language with at least one constant, and let Φ be a set of ∀∗ L-sentences including the equality axioms for L. Then Φ is unsatisfiable iff some finite set Φ0 of L-ground instances of sentences in Φ is propositionally unsatisfiable.

Herbrand Theorem only applies to determining the satisfiability of ∀∗ sentences. In other cases, we need Skolemization.

Definition 2.2. Let φ be a first-order sentence in prenex normal form. We construct the functional form of φ by removing each existential quantifier ∃y in the prenex and replacing y in the formula by f(x1, . . . , xn), where f is a new function symbol, and x1, . . . , xn are the universally quantified variables that precede ∃y in the prefix. To form the functional forms of a set of sentences, it is necessary to make every Skolem function symbol introduced distinct from all Skolem function symbols in all other formulas.

Theorem 2.3. A set Φ of sentences is satisfiable iff the set of functional forms of sentences in Φ is satisfiable.

2.2 The Situation Calculus

We will not go over the language of the situation calculus here except to note 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 proper subhistory of s′ ; a binary predicate Poss(a, s) meaning that action a is possible in situation s; a finite number of action functions; a finite number of relational and functional fluents, i.e., predicates and functions taking a situation term as their last argument.

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 τ. A situation s is executable if it is possible to perform the actions in s one by one:

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, including a second-order induction axiom for situations:

1. Dap contains a single precondition axiom for all actions of the form Poss(a, s) ≡ Π(a, s), where Π(a, s) is uniform in s.
2. 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.
3. Duna is the set of unique names axioms for actions.
4. DS0 , the initial KB, is a set of sentences uniform in S0.

Actions in many domains have only local effects in the sense that if an action A(⃗c) changes the truth value of an atom F(⃗e, s), then ⃗e is contained in ⃗c. This contrasts actions that have non-local effects such as moving a briefcase, which will also move all the objects inside the briefcase without having mentioned them. We skip the the formal definition here.

We say that Dap and Dss are essentially quantifier-free if for each action function A(⃗y) and each fluent F, by using Duna, both Π(A(⃗y), s) and ΦF (⃗x, A(⃗y), s) can be simplified to quantifier-free formulas.

Definition 2.4. A basic action theory is simple if every action is local-effect, Dap and Dss are essentially quantifierfree, and DS0 is a consistent set of ∀∗ formulas.

Example 2.5. Below are parts of a simple BAT:

P oss(stack(x, y), s) ≡ holding(x, s) ∧ clear(y, s) ∧ x ̸= y on(x, y, do(a, s)) ≡ a = stack(x, y)∨

on(x, y, s) ∧ a ̸= unstack(x, y)

holding(x, do(a, s)) ≡

We assume that D is simple throughout this paper.

An important computational mechanism for reasoning about actions is regression. Here we define a one-step regression operator for simple action theories, and state a simple form of the regression theorem [Reiter, 2001].

Definition 2.6. 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.

2.3 State Constraints and State Invariants

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 2.8. Given D and a formula φ(s), φ(s) is a state constraint for D if D |= ∀s.Exec(s) ⊃ φ(s).

So state constraints are formulas which hold in all executable situations. Since D includes a second-order induction axiom for situations, verifying state constraints is a secondorder reasoning task. We make

an extra component of D. We also abuse DSC as the conjunction of the elements in DSC.

Our approach exploits verified state constraints to verify other constraints, so we have a slightly different definition of state invariants below:

Definition 2.9. Let Dvc be a set of formulas uniform in s, called the background information. A formula φ(s) is a state invariant for D wrt Dvc if

Given the background information Dvc, state invariants are those that if true in a situation, will be true in all successor situations. Clearly, verifying state invariants is a first-order reasoning task. We will use DSC to collect those verified constraints, and use it as the background information. Obviously, if φ(s) is a state invariant wrt some subset of DSC, then φ(s) is a state invariant wrt DSC.

Definition 2.10. We say φ(s) is a state invariant for D, if φ(s) is a state invariant wrt a set of state constraints for D.

The following shows closure properties of constraints.

Proposition 2.11. 1. φ(s) ∧ψ(s) is a constraint iff both φ(s) and ψ(s) are constraints.

1. If φ(s) is a constraint, then so is φ(s) ∨ψ(s).

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

Proposition 2.12. If every element of DSC is an invariant, DS0 |=FOL ϕ(S0), and ϕ(s) is an invariant, then ϕ(s) is a constraint.

Our approach verifies a constraint by strengthening it to be an invariant, which is put into DSC, so it can ensure that every element of DSC is an invariant.

3 Theoretical Foundations

In this section, we introduce the theoretical foundations of our work, i.e., the concepts of joint constraints and derivants, and incomplete reasoning based on Hebrand Theorem.

3.1 Joint Constraints and Derivants

We now introduce the most important concepts of this paper.

Definition 3.1. An invariant constraint is a constraint which is also an invariant. If ϕ(s) ∧ η(s) is an invariant constraint, we call ϕ(s) a partial invariant constraint. If ϕ(s) ∧ η(s) is a partial invariant constraint and η(s) is not logically implied by ϕ(s), we call η(s) a joint constraint for ϕ(s).

We collects a set of invariant constraints in DSC. Given a ∀∗ partial invariant constraint, we will strengthen it with a sequence of joint constraints to approach an invariant constraint. Below we show how to obtain such joint constraints.

By Proposition 2.11 and Theorem 3.2, we have

Proposition 3.3. If ϕ(s) is a constraint for D, then for any action function A(⃗x), the following is also a constraint:

Let ϕ(s) be a formula ∀⃗yφ(s), where φ(s) is quantifierfree. As D is simple, ˆRD[Poss(A(⃗x), s) ⊃ ϕ(do(A(⃗x), s))] can be put into a formula ∀⃗yψ(s), where ψ(s) is quantifierfree and can be put into CNF. So we have the definition below:

Definition 3.4. Let ϕ(s) be a ∀∗ formula. We transform ˆRD[Poss(A(⃗x), s) ⊃ ϕ(do(A(⃗x), s))] into a prenex CNF formula. We call each conjunct a derivant of ϕ(s).

By Proposition 2.11, we have the following proposition which shows that the derivants of constraints are constraints.

Proposition 3.5. Let ϕ(s) be a constraint, and C(s) a derivant of ϕ(s). Then C(s) is a constraint.

Below we show that the derivants of a partial invariant constraint ϕ that are not implied by ϕ are its joint constraints.

Theorem3.6 (MainTheorem). If ϕ(s)∧η(s) is an invariant constraint, and C(s) is a derivant of ϕ(s), then

1. ϕ(s) ∧C(s) is a partial invariant constraint.

Suppose that ϕ(s) is a partial invariant constraint but not an invariant. Our approach will choose a derivant C(s) of ϕ(s) such that ̸|=FOL ∀s.DSC ∧ϕ(s) ⊃ C(s), so ϕ(s) ∧C(s) is strictly stronger than ϕ(s). Thus our approach will strictly strengthen ϕ(s) towards an invariant constraint.

The notion below is used to describe our algorithms.

Definition 3.7. The length of a CNF formula F, written |F|, is defined to be the sum of the length of the clauses.

3.2 Incomplete Reasoning via Herbrand Theorem

In verifying state constraints, we need to check first-order entailment of ∀∗∃∗ sentences, which can be reduced to checking the satisfiability of a set of sentences. By Skolemization, this can be reduced to checking the satisfiability of the functional forms of the sentences, which is a set of ∀∗ sentences.

We use an incomplete algorithm to check the satisfiability of a set of ∀∗ L-sentences. We first test the satisfiability of a subset of L-ground instances using some finite set H0 of terms in L. If it is satisfiable, we test the satisfiability of a larger subset of L-ground instances, using a finite set H1 of terms such that H0 ⊂ H1. We repeatedly do so with larger subset of terms until unsatisfiability is confirmed or some bound is reached. We now formalize the above idea.

Definition 3.8. Let L be a first-order language with at least one constant symbol. We define partial Herbarnd universe for L as follows: HL 0 is the set of constants of L. For n ≥ 0, HL n+1 is the union of HL n and the set of terms f(⃗t) such that f is a function of L, and each ti belongs to HL n .

Let Φ be a set of ∀∗ L-sentences, and H a set of ground terms of L. We use gnd(Φ)|H to denote the set of L-ground instances of sentences in Φ using ground terms from H.

By Theorem 2.1 and Theorem 2.3, we obtain a theorem to establish entailment of ∀∗∃∗ sentences as follows.

Theorem 3.9. Let Ψ be a set of ∀∗∃∗ sentences, and ψ a ∀∗∃∗ sentence. Let Φ be the set of Skolem functional forms of Ψ∪{¬ψ}, and L the language of Φ. Then Ψ |=FOL ψ iff there exists some n such that gnd(Φ)|HL n is unsatisfiable.

We use Ψ |=nFOL ψ to denote that gnd(Φ)|HL n is unsatisfiable. We remark that all ∀∗∃∗ constraints in this paper are verified by gnd(Φ)|HL 1 , so this method is empirically effective.

4 Algorithms

Below, we use ψ = φ(s) ↑ s to mean that ψ is the formula obtained from φ(s) by replacing each fluent atom F(⃗t, s) by F(⃗t), and we say ψ is situation-suppressed. We use ψ[s] to denote the formula obtained from ψ by restoring the situation argument s to all predicates in ψ. Note that all input and output formulas of our algorithms are situation-suppressed.

4.1 Verifying State Constraints

Algo. 1 verifies if the input ∀∗ formula φ is a state constraint for the input BAT D. If φ is verified to be a state constraint, the algorithm outputs an invariant constraint subsuming φ.

Algorithm 1: veri SC(φ, D,M, β)

input : A ∀∗ formula φ, a BAT D, a setMof small initial models, a bound β output: an invariant constraint subsuming φ, or False, or Non-deter 1 ∆← {φ[s]} 2 while True do 3 remove a shortest formula ϕ(s) from∆ 4 if |ϕ(s)| ≥ β then return Non-deter 5 if ∃M ∈M.M ̸|= ϕ(S0) or DS0 ̸|=FOL ϕ(S0) then 6 if ϕ(s) is integral then return False 7 else continue 8 IS SI ← T rue 9 foreach action function A(⃗x) do 10 re ← ˆRD[P oss(A(⃗x), s) ⊃ ϕ(do(A(⃗x), s))] 11 C1(s) ∧ . . . ∧ Cn(s) ← cnf(re) 12 if ∃Ci(s). ̸|=FOL ∀⃗x, s.ϕ(s) ∧ DSC ⊃ Ci(s) then 13 IS SI ← False 14 foreach η(s) ⊆ Ci(s) do 15 ∆ ← ∆ ∪ {∀⃗x, s.ϕ(s) ∧ η(s)} 16 break 17 if IS SI = True then return ϕ(s) ↑ s

Now we illustrate the two other inputs of the algorithm: a set Mof small initial models and a bound β. Given ϕ(s), in verifying whether ϕ(s) is a constraint, we might strengthen it, so we will have to verify longer and longer formulas. We believe that most meaningful constraints can be proved after being strengthened a few times, so we use β to bound |ϕ(s)| in Line 4. To speed up the evaluation of DS0 |=FOL ϕ(S0), we use a small setMof small models of DS0 in Line 5. If ϕ(S0) is falsified by a model, it cannot be entailed, and this improves efficiency greatly. We say a member of ∆ is integral if it is the input formula or it is obtained in Line 15 with η(s) = Ci(s).

Here's the work flow. In Line 3 the shortest formula is selected. In Line 11, the formula re is transformed into CNF, C1(s) ∧ . . . ∧ Cn(s). Line 12 successfully proves that |=FOL ∀⃗x, s.DSC∧ϕ(s)∧Poss(A(⃗x), s) ⊃ ϕ(do(A(⃗x), s), or it picks up a clause Ci(s) not entailed by DSC ∧ϕ(s) and use it to strengthen ϕ(s). Line 14 considers all subsets of Ci(s), and this is not very much a problem to efficiency, since in practice, |Ci(s)| is relatively small. The motivation is that it is likely that both Ci(s) and a subset η(s) of it are joint constraints of ϕ(s), and we prefer η(s) to Ci(s) for both understandability and efficiency reasons.

The following theorem shows that Algorithm 1 is sound.

Theorem 4.1. Given an input φ, if Algorithm 1 returns ϕ, then ϕ[s] is an invariant constraint subsuming φ[s]; if it returns False, then φ[s] is not a constraint.

Algo. 2 verifies if an input ∀∗∃∗ formula is a constraint by checking if itself is an invariant. In the algorithm, we apply the |=nFOL entailment relation as defined after Theorem 3.9, which we implement with a SAT solver. Below is the soundness theorem for Algo. 2.

input : A ∀∗∃∗ formula φ, D,Mas before output: True, False, or Non-deter 1 if ∃M ∈M.M ̸|= φ[S0] or DS0 |=nFOL ¬φ[S0] then 2 return F alse 3 if DS0 ̸|=nFOL φ[S0] then return Non-deter 4 foreach action function A(⃗x) do 5 ξ(s) ← ˆRD[Poss(A(⃗x), s) ⊃ ϕ(do(A(⃗x), s))] 6 if ̸|=nFOL ∀⃗x, s.DSC ∧ ϕ(s) ⊃ ξ(s) then 7 return Non-deter

Algorithm 2: ex query(φ, D,M) 8 return True

4.2 Enumerating State Constraints

Algo. 3 enumerates all ∀∗ formulas containing one or two literals, and collects those which are verified to be constraints, together with their joint constraints. Here the input Γ is the set of candidate formulas, and all other inputs have the same meanings as before. In Line 2, formulas in Γ falsified by a model of M or not entailed by DS0 are eliminated. From Line 5 to Line 10 we traverse Γ and move those verified constraints to both Θ and DSC. If a new constraint is found, then MORE SC will be assigned True in Line 8, and we repeatedly traverse Γ until no more constraints are found.

Theorem 4.3. Algorithm 3 returns a set of state constraints.

5 Experimental Results

We implemented the procedures outlined above in gcc (Version 4.7.2) and SWI-Prolog (Version 5.10.4). All experiments were run on a machine with Intel(R) Core(TM)2 Duo with 2.10 GHz CPU and 2.00GB RAM under Linux. Note that our experiments were not designed for comparison with other approaches, but to show that our approach indeed produces effective results in a reasonable amount of time.

We tested our method with the blocks world, logistics and satellite domains. In all our experiments, we assume that DS0 is represented by a finite set of finite initial models, so we reduce DS0 |=FOL ϕ(S0) to model checking. Below are the models used in blocks world (each model has exactly 3 blocks):

Algorithm 3: enum SC(Γ, D,M, β)

input : A set Γ of ∀∗ formulas, and D,M, β as before output: A set Θ of state constraints 1 Θ← ∅ 2 remove from Γ γ such that ∃M ∈M.M ̸|= γ[S0] or DS0 ̸|=FOL γ[S0] 3 repeat 4 MORE SC←False 5 foreach γ ∈ Γ do 6 sc ← veri SC(γ, D,M, β) 7 if sc ̸= False and sc ̸= Non-deter then 8 MORE SC ← T rue 9 add sc into both Θ and DSC 10 remove γ from Γ 11 until not MORE SC; 12 return Θ

1. {clear(b1), clear(b2), clear(b3), ontable(b1), ontable(b2), ontable(b3), handempty};
2. {clear(b1), on(b1, b2), clear(b3), ontable(b2), ontable(b3), handempty};
3. {clear(b1), holding(b1), clear(b2), ontable(b2), clear(b3), ontable(b3)}.

For each domain, we first use Algo. 3 to enumerate constraints, and then with these constraints as the background information, we use Algo. 1 and Algo. 2 to process ∀∗ and ∀∗∃∗ formulas, respectively. Experiments show that all invariants discovered by Lin [2004] can be verified by our method.

5.1 ∀∗ State Constraints

Blocks World

We used Algo. 3 and found the following constraints:

{¬clear(x) ∨ ¬on(y, x), ¬holding(x) ∨ ¬on(y, x),

¬holding(x) ∨ ¬on(x, y), ¬on(x, y) ∨ ¬on(y, x),

¬on(x, y) ∨ ¬ontable(x), ¬holding(x) ∨ ¬handempty,

¬holding(x) ∨ ¬ontable(x), ¬holding(x) ∨ clear(x)}.

Some longer constraints are discovered during the process:

{on(x, z) ∧ on(y, z) ⊃ x = y, on(x, y) ∧ on(x, z) ⊃ y = z,

holding(x) ∧ holding(y) ⊃ x = y}.

We also found some other constraints not discovered by Lin: {¬on(x, x), ¬on(x, y) ∨ ¬on(y, x)}.

Logistics Domain

Lin regarded type information as domain specific knowledge, but we also found them. Some examples are:

¬city(x) ∨ ¬location(x), ¬airplane(x) ∨ ¬truck(x).

Besides type information, we also found the constraints:

{¬in(x, y) ∨ ¬city(x), ¬in(x, y) ∨ ¬truck(x),

One constraint containing 3 literals is discovered:

at(x, y) ∧ at(x, z) ⊃ y = z.

Satellite Domain

This was first introduced by AIPS'00. It involves planning and scheduling of observation tasks performed by instruments on some satellites. Any satellite can carry a few instruments, denoted by the predicate on board. If any instrument is turned on (power on), it will make its satellite's power no longer available (power avail) for other use. Different instruments support (supports) different modes. Before an instrument performs its observation task (take image), it must be able to calibrate on some object (calibration target), causing the state of ready (calibrated).

Below the first two constraints were discovered while the third one was verified. They states that (1) if an instrument on a satellite is powered on, then the electricity of that satellite will not be available for other use; (2) one instrument can be located on only one satellite; and (3) at most one instrument on a satellite can be powered on.

{on board(x1, x2) ∧ power on(x1) ⊃ ¬power avail(x2), on board(x1, x2) ∧ on board(x1, x3) ⊃ x2 = x3, on board(x1, x3) ∧ power on(x1)

∧ on board(x2, x3) ∧ power on(x2) ⊃ x1 = x2}.

5.2 Discovering Joint Constraints

Algo. 1 iteratively strengthens the input formula φ, and when it verifies φ to be a constraint, it also discovers φ's joint constraints. In contrast Lin enumerates candidate formulas of the given syntactic forms and check if they are indeed invariants.

Example 5.1. 1. We were to test whether

φ1 = holding(x) ⊃ ¬ontable(x) is a state constraint.

1. φ1 is not proved to be a state invariant, so the system strengthened it with φ2 = ¬on(x1, x2) ∨ ¬ontable(x1).
2. Again, φ1 ∧ φ2 is not a state invariant so the system strengthened it with φ3 = ¬on(x1, x2)∨¬holding(x1).
3. After getting φ4=¬on(x1, x2)∨¬on(x1, x3)∨x2 = x3, φ1 ∧ . . . ∧ φ4 was proved to be a state invariant, and thus, φ1, . . . , φ4 were all proved to be state constraints.

You see, all discovered constraints are succinct and intuitive.

5.3 ∀∗∃∗ State Constraints

Lin [2004] discovered the following constraints in the blocks world and logistics domains:

{holding(x) ∨ clear(x) ∨ (∃y)on(y, x),

ontable(x) ∨ holding(x) ∨ (∃y)on(x, y),

handempty ∨ (∃x)holding(x), }

and

{∀(x, package).∃(y, vehicle)in(x, y) ∨ ∃(y, place)at(x, y), ∀(x, palce).∃(y, city)inCity(x, y), ∀(x, vehicle).∃(y, place)at(x, y)}.

Using |=1FOL , our approach verified them and the following: {∀x∃y.on board(x, y),∀x∃y.supports(x, y),

∀x∃y.calibrated(x) ⊃ calibration target(x, y),

∀x∃y.power avail(x) ∨ on board(y, x) ∧ power on(y)}.

5.4 Performance

Table 1 shows the time costs in verifying constraints in the three domains (B.W. abbreviates blocks world). The column Enum Binary shows the time of enumerating all unary and binary constraints using Algo. 3, in terms of minutes. The columns ∀∗ formulas and ∀∗∃∗ formulas both contain two sub-columns: Min and Max, where Min is the minimal time cost of verifying a constraint among those we experimented with, and Max shows the maximal. When enumerating constraints, the values of β are as shown in Table 2. However, when verifying a single constraint, we use a sufficiently large bound. In both Table 1 and Table 2, when we verify a ∀∗ formula, we let DSC = ∅, i.e., we do not consider background information. When we verify a ∀∗∃∗ -formula, we let DSC be the set of constraints returned by Algo. 3, i.e., we verify them after enumerating constraints using Algo. 3.

Table 1 shows, that the difference between Max and Min for verifying a ∀∗ constraint using Algo. 1, is much greater than that for verifying a ∀∗∃∗ constraint using Algo. 2. This is because Algo. 1 iteratively strengthens a formula φ(s) until an invariant is obtained, while Algo. 2 returns Non-deter once φ(s) is not proved to be an invariant. In verifying ∀∗ constraints, B.W. has the maximal time difference while satellite domain has the minimal, because B.W. is the most structured domain, and some constraints entangle dramatically. One would notice that the maximal time cost of verifying one constraint in B.W. even surpasses the total time of enumerating constraints. That is because Algo. 3 exploits previously verified constraints to speed up further verifications, so it can avoid many costly operations of discovering joint constraints.

Table 2 shows how much time Algo. 1 has spent before returning False or Non-deter. Here Min and Max have the same meanings as above. In logistics and satellite domains, no formulas are non-determined, that is, all formulas are verified or rejected, so we fill '-' in the respective grids. This shows that Algo. 1 happens to be complete in these domains.

In B.W., it takes Algo. 1 quite long (≥6s) before Non-deter is returned, and the worst case needs 123s. When Algo. 1 returns False, it takes very short time in all three domains, because most rejected formulas are falsified by one of the initial models and are rejected immediately.

Below we list some non-determined formulas in blocks world when we use Algo. 3 to enumerate constraints:

{clear(x) ∨ ontable(x), clear(x) ∨ handempty,

clear(x) ∨ ¬on(x, y), clear(x) ∨ ¬holding(x), ontable(x) ∨ ¬on(y, x), ¬on(x, y) ∨ ¬holding(y), handempty ∨ ¬on(x, y), ¬on(x, y) ∨ ¬on(y, x)}.

In fact, none of them is a constraint except the last one. We then ran Algo. 1 on ¬on(x, y)∨¬on(y, x) with β = 14, and it was verified to be a constraint. In fact it costs us the most time - 1402.8s as Table 1 shows. This indicates that its verification depends on the discovery of quite a few joint constraints.

6 Conclusions

Various other communities, e.g., model-checking, program verification and planning communities, are also interested in state constraints. We discuss two typical works below.

Bradley and Manna [2007; 2011] developed a sound and complete algorithm to verify state constraints on large circuits. In contrast, we are verifying constraints on a first-order dynamic system, and it is trivial to reduce our framework to theirs, when we restrict our domains to be finite. Both works strengthen a state constraint to be an invariant constraint, and prefer shorter clauses. They used fixpoint techniques to compute minimum useful clauses while we use models to help eliminate useless clauses.

Rintanen [2000] applied a procedure to a set Σi of candidate formulas to generate a refined set Σi+1 of formulas iteratively, until Σi = Σi+1, so as to obtain a set of invariant constraints. His method is efficient when every candidate formula is a unit or binary clause, and it is guaranteed that his algorithm terminates in polynomial time. Like Lin, he combined formulas and verified if the conjunctions are invariants.

In this paper, we have developed a sound but incomplete method for automatical verification and discovery of ∀∗∃∗ constraints. Our method takes a single formula as the input, and strengthens it to be an invariant with joint constraints. We experimented with the blocks world, logistics and satellite domains, and the results showed that, our method is efficient and able to verify all constraints discovered in [Lin, 2004].

Now we summarize our contributions. Firstly we have developed a practically effective method with solid theoretical foundations for verifying if a given ∀∗∃∗ formula is a state constraint. Secondly, if a state constraint is not proved to be a state invariant, our method will systematically strengthen it with derivants and hence discover joint constraints. Thirdly, so far as we know, we are the first to propose a method with soundness guarantee for verifying ∀∗∃∗ constraints. Lastly, experiments show that practically meaningful and useful constraints can be efficiently verified with our approach, and succinct and intuitive joint constraints can be discovered. Here, the second and the third points distinguish our work from [Lin, 2004]. Another difference is: our method is based on Herbrand Theorem and Skolemization and implemented with a SAT solver, while Lin's work is based on exhaustive search in selected small domains.

However, our work has two limitations. Firstly our method can only verify partial invariant constraints. Secondly when verifying ∀∗∃∗ constraints, our method is of poor scalability.

There are at least two topics for future research. Firstly, our current approach to strengthening formulas can only be applied to ∀∗ constraints, so we will extend our method to handle ∀∗∃∗ constraints. Secondly, we would like to know under what conditions, a state constraint can be strengthened to be a state invariant, so we know the conditions under which our algorithms are complete.

Acknowledgments

We thank the anonymous reviewers for helpful comments. This work was supported by the Natural Science Foundation of China under Grant No. 61073053.