Automatic Verification of FSA Strategies via Counterexample-Guided Local Search for Invariants

1 Introduction

Strategy representation and reasoning has received much attention over the past years. The two most popular strategic logics are Alternating-time Temporal Logic (ATL) [Alur et al., 2002] and Strategy Logic (SL) [Chatterjee et al., 2010]. In ATL, strategies are treated implicitly: the formula 〈〈A〉〉φ expresses that coalition A has a strategy to ensure φ hold. In SL, a strategy is an explicit first-order object which is a function from sequences of states to actions. Model-checking for ATL is in PTIME, while model-checking for SL is nonelementarily decidable. MCMAS [Lomuscio et al., 2009] and MCMAS-SLK [Cerm´ak et al., 2014] are representative model checking tools for ATL and SL respectively.

In this paper, we are concerned about the representation and reasoning of general strategies that solve a class of (possibly infinitely many) games with similar structures, represented by a basic action theory in the situation calculus [Reiter, 2001]. A related problem is generalized planning where a single plan works for possibly infinitely many similar planning problems [Levesque, 2005; Srivastava et al., 2008]. To illustrate our problem, consider the Chomp game. As shown in Figure 1, cookies are laid out on a rectangular grid of an arbitrary size.

∗Corresponding author

The cookie in the top left position (1,1) is poisoned. Two players take turns making moves: at each move, a player eats a remaining cookie, together with all cookies to the right or below it. When the grid is square, a (general) winning strategy for player 1 is this: First, eat the cookie in position (2,2); then when the opponent eats the cookie in position (x, y), respond with eating the cookie in position (y, x).

To represent generalized plans that solve multiple planning instances, Hu and Levesque [2011] proposed FSA (Finite State Automaton) plans. Inspired by this work, in this paper, we propose to represent a general strategy by an FSA with edges labeled by restricted programs of Golog [Levesque et al., 1997]. FSA representation of strategies has the advantages of ease to represent nested loop structures and amenability to algorithmic operations. We formalize the semantics of FSA strategies in the situation calculus, by making use of second-order logic.

In this paper, we explore the automatic verification of FSA strategies, in particular, verifying if an FSA strategy is a winning strategy wrt a basic action theory in the situation calculus. Since this is a (second-order) theorem-proving task, we propose a sound but incomplete method via counterexampleguided local search for appropriate invariants, which can be checked with first-order theorem proving. For an FSA strategy, an invariant is a labelling of each strategy state with a formula so that if the formula is true in the state, in any successor state, the label formula will be true. The method of counterexample-guided refinement is widely used in the formal methods community, e.g., CEGAR (Counter-Example Guided Abstraction Refinement) [Clarke et al., 2000; 2003]. The idea is: first generate an initial abstraction; if it does not serve the purpose, we get a counterexample and use it to refine our abstraction, and then repeat the process.

We implemented our method and experimented on twoplayer domains from the combinatorial game literature. We also tested our method with single-agent domains from the planning literature by adapting them to our framework. Our system can successfully verify most of them within a reasonable amount of time.

2 Preliminaries

In this section, we introduce the situation calculus, Golog programs, regression, and small model progression.

The situation calculus is a many-sorted first-order logical language with limited second-order features [Reiter, 2001]. In a situation calculus language, there are three disjoint sorts: action for actions, situation for situations and object for everything else. The symbol S0 denotes the initial situation; do(a, s) is a binary function representing the situation resulting from performing action a in situation s; the relation Poss(a, s) states that it is possible to perform action a in situation s. There are action functions, e.g., put(x, y). A fluent is a special relation/function whose values vary from situation to situation and is denoted by a relation/function whose last argument is a situation term. If a formula refers to a particular situation τ , we call it uniform in τ . A uniform formula φ with all situation arguments removed is called a situationsuppressed formula, and φ[s] denotes the formula obtained from φ by restoring s as the situation arguments to all fluents.

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 relational fluent, of the form

and one for each functional fluent, of the form

where ΦF (⃗x, a, s) and Φf (⃗x, y, a, s) are uniform in s.

1. Duna is the set of unique names axioms for actions.

Golog is a high-level programming language for representing complex actions. The formal semantics of Golog is specified by an abbreviation Do(δ, s, s′ ), meaning that situation s will be updated to s′ after executing program δ. Do(δ, s, s′ ) is inductively defined as follows:

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

Regression is an important computational mechanism for reasoning about actions. Here we present the one step regression operator.

Definition 1 Given a BAT D, we use R[φ] to denote the formula obtained from φ by the following steps:

1. For each functional fluent term f(⃗t, do(α, σ)), replace the current formula ψ with (∃y).Φf(⃗t, y, α, σ) ∧ ψ[f(⃗t, do(α, σ))/y], where ψ[t/y] denotes the result of replacing all occurrences of t in ψ by y.
2. Replace each fluent atom F (⃗t, do(α, σ)) with ΦF (⃗t, α, σ).
3. Replace each atom Poss(α, σ) with Π(α, σ).
4. Further simplify the result by using Duna.

Li and Liu [2015] extended the regression of formulas wrt primitive actions to that wrt programs. Here we omit the case of iteration since we do not need it in this paper.

Definition 2 Let φ(s) be a formula uniform in s. The regression of φ(s) wrt program δ, written R[φ(s), δ], is defined as:

• R[φ(s), ψ?] .= ψ[s] ⊃ φ(s).
• R[φ(s), α] .=R[Poss(α, s) ⊃ φ(do(α, s))].
• R[φ(s), δ1; δ2] .=R[R[φ(s), δ2], δ1].
• R[φ(s), (πx)δ(x)] .= (∀x)R[φ(s), δ(x)].
• R[φ(s), δ1|δ2] .=R[φ(s), δ1] ∧R[φ(s), δ2].

Based on Proposition 1, by induction, it is easy to prove:

Proposition 2 Let δ be a Golog program not involving nondeterministic iteration. We have:

A small model can be represented as a finite set of ground atoms under the closed-world assumption. Li and Liu [2015] presented the notion of small model progression, and use prog[M, δ] to denote the set of small models resulting from M by executing δ. The formal definition is as follows:

Definition 3 Given a small model M with domain D 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. {M ′ } if M[s] |= Poss(α, s), where M ′ is the model obtained from M by applying the effects of α.
• prog[M, ψ?] = 1. ∅ if M[s] ̸|= ψ[s]. 2. {M} if M[s] |= ψ[s].
• prog[M, δ1|δ2] = prog[M, δ1] ∪ prog[M, δ2].
• prog[M, δ1; δ2] = prog[prog[M, δ1], δ2].

· prog[M, (πx)δ(x)] = ⋃{prog[M, δ(c)]|c ∈ D}. When M is a set of small models, we define prog[M, δ] = ⋃{prog[M, δ]|M ∈ M}.

in row x.

w(x, s)

^ y < j_

w(x, s) < j

N > 1

n(p)

' strategies,

we propose

og program

esults in the

, E, q0) s.t.

itial state;

, where q is

is the label,

rimitive ac-

itional strat-

ing at q are

aving q are

hat we use

s allows for

a player p

g. The exe-

0. When the

q0 , perform

A composi-

game. The

e is in state The FSA strategy shows how player 1 play for the chomp game. Player 1 tries to constantly perform an action depending on the labelled program ⌧ and the current situation and stays in state Q0. Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI-19)

In the following, we formalize the semantics of FSA strategies. Given an FSA strategy S, we first introduce a Figure 2: An FSA strategy and its composite strategy

transition relation TS(q, s, q0 , s0 ), meaning that from situation s, it is possible to reach situation s0 by executing a program starting at state q and ending at state q0 . 3 FSA Strategies In this section, we formalize the concept of FSA strategies in

Definition 6 Given an FSA strategy S = (Q,E,Q0) where Q ✓ Q, we use TS(q, s, q0 , s0 ) as abbreviation for the following formula: Wg ⌧!g0 g = q^g0 = q0^Do(⌧, s, s0 ). the situation calculus. We focus on combinatorial games [Ferguson, 2014], i.e., two-player turn-based games which always end in a finite number of moves.

It is possible that a strategy is incomplete in the sense that when the opponent adopts the null strategy, there might be situations where the player is in a state q where no program starting at q is executable. We add a special action πa.a, meaning doing any executable action. Its formal semantics is defined as follows: Do(πa.a, s, s′ ) .= ∃a.Poss(a, s) ∧ s′ = do(a, s). We now formalize the chomp game.

For a compositional strategy S, we define the reflexive transitive closure of TS : intuitively, T ⇤ S (q, s, q0 , s0 ) means that from situation s, it is possible to reach situation s0 by following the compositional strategy. Definition 7 Given an FSA compositional strategy S = (Q,E,Q0) where Q ✓ Q, we use T ⇤ S (q, s, q0 , s0 ) as abbreviation for 8R.{. . . ⊃ R(q, s, q0 , s0 )}, where . . . is the conjunction of the universal closure of the following: · R(q0 , s0 , q0 , s0 ); · R(q, s, q0 , s0 ) ^ TS(q0 , s0 , q00 , s00 ) ⊃ R(q, s, q00 , s00 ). We make the following extensions of the situation calculus and a basic action theory D: We introduce a new sort state, a countable infinite set of state constants Q = {Q0, Q1, . . .}, and unique name axioms of the form Qi ̸= Qj , for i ̸= j. We introduce a new sort player, two player constants P1 and P2, together with the axiom ∀p.(p = P1 ∨ p = P2) ∧ (P1 ̸= P2). We use a relational fluent turn(p, s), meaning in situation s, it is p's turn to play. We add the axioms: turn(p, do(a, s)) ≡ ¬turn(p, s) and turn(P1, S0) ∧ ¬turn(P2, S0). We introduce abbreviations end(s), meaning the game ends in situation s, and win(p, s), meaning p wins in situation s.

Example 1 We use two constants N and M to denote the size of the rectangular grid. Fluent ch(x, y, s) means there is a cookie at position (x, y). Action eat(p, x, y) means player p eats the cookie at position (x, y) together with all cookies to the right or below it. Fluent last(x, y, s) means the last action is eat(p, x, y) for some player p. In addition to the second-order axiomatization of Peano arithmetic, we have the following axioms:

P oss(eat(p, x, y), s) ≡ turn(p, s) ∧ ch(x, y, s) ch(x, y, do(a, s)) ≡ ∃p, i, j.a = eat(p, i, j) ∧ (i > x ∨ j > y) last(x, y, do(a, s)) ≡ ∃p.a = eat(p, x, y) ch(x, y, S0) ≡ 0 < x ≤ N ∧ 0 < y ≤ M win(p, s) .= turn(p); end(s) .= ¬ch(1, 1, s)

We use Chomp NxN (resp. 2xN) to represent the chomp game with square (resp. two row) grids, and add the Initial Situation Axiom M = N (resp. M = 2).

Note that although each chomp game is finite, since there is no bound on the size of the game, there are infinitely many chomp games.

We say that a Golog program is single-step if its execution always results in the execution of a single primitive action.

Definition 4 An FSA strategy is a tuple S = (Q,E, q0) s.t. Q is a finite set of states, and q0 ∈ Q is the initial state; E

is a finite set of edges of the form q τ→ q′ , where q is the starting state, q′ is the ending state, and τ is the label, which is a single-step Golog program.

A notable difference from FSA plans is that we use singlestep Golog programs as edge labels. This allows for more compact representation of strategies.

We say that S is a strategy for player p if all primitive actions are actions of p. We say that S is a compositestrategy if for any state q, all primitive actions ending at q are actions of a player and all primitive actions leaving q are actions of the other player.

Intuitively, a state of an FSA strategy S for a player p represents a mental state of p for decision making. The execution of S is as follows. Initially, p is in state q0. When the player is in state q, she can choose an edge q τ→ q′ , perform τ and move to q′ . Intuitively, a state of an FSA composite strategy C represents mental states of both players.

Figure 2(a) shows an FSA strategy with a single state q0 and a single edge from q0 to q0 labeled with πa.a. It indicates the strategy for a player where the player simply takes any executable action. We call such a strategy the null strategy. Strategies for both players can be composed to form a composite strategy, as defined below:

Definition 5 Given an FSA strategy S1 = (Q1,E1, q1 0 ) for player 1 and an FSA strategy S2 = (Q2,E2, q2 0 ) for player 2, we define their composition strategy S = (Q,E, q0) as follows: Q = Q1 × Q2 × {1, 2}, q0 = (q1 0 , q2 0 , 1), and for any q1 ∈ Q1, q2 ∈ Q2, (q1, q2, 1) τ→ (q′1 , q2, 2) iff q1 τ→ q′1 in S1, and (q1, q2, 2) τ→ (q1, q′2 , 1) iff q2 τ→ q′2 in S2.

Example 1 cont'd Figure 1(b) shows an FSA strategy of player 1 for the Chomp NxN game. Player 1 begins with action eat(P1, 2, 2) and moves to state q1. In state q1, for P2's action eat(P2, x, y), player 1 responds with eat(P1, y, x) and stays in state q1. Figure 1(c) is the result of composing the above strategy with the null strategy.

In the following, we formalize the semantics of FSA strategies. Given an FSA strategy S, we first introduce a transition relation TS(q, s, q′ , s′ ), meaning that from situation s, it is possible to reach situation s′ by executing a program starting at state q and ending at state q′ .

Definition 6 Given an FSA strategy S = (Q, E, Q0) where Q ⊆ Q, we use TS(q, s, q′ , s′ ) as abbreviation for the following formula: ∨g τ→g′∈E g = q ∧ g′ = q′ ∧ Do(τ, s, s′ ).

For a composite strategy S, we define the reflexive transitive closure of TS : intuitively, T ∗ S (q, s, q′ , s′ ) means that from situation s, it is possible to reach situation s′ by following the composite strategy.

Definition 7 Given an FSA composite strategy S = (Q, E, Q0) where Q ⊆ Q, we use T ∗ S (q, s, q′ , s′ ) as abbreviation for ∀R.{φ ⊃ R(q, s, q′ , s′ )}, where φ is the conjunction of the universal closure of

• R(q, s, q, s), and

It is possible that a strategy is incomplete in the sense that when the opponent adopts the null strategy, there might be

• R(q, s, q′ , s′ ) ∧ TS(q′ , s′ , q′′ , s′′ ) ⊃ R(q, s, q′′ , s′′ ).

situations where the player is in a state q where no program starting at q is executable.

Definition 8 Given a BAT D and an FSA strategy S for player p, we say S is complete if the composition C of S and the null strategy satisfies D |=

It is easy to make an incomplete strategy complete as follows. We add a special dead state. For each state q, we add an edge from it to the dead state labeled with the program φq?; πa.a, where φq is the negation of the disjunction of the executability condition of each program leaving q.

We now define the concept of winning strategies. Intuitively, a strategy for player p is a winning strategy if Cond1: p always wins no matter what strategy the opponent adopts, which is equivalent to Cond2: p always wins when the opponent adopts the null strategy. To see why, Cond1 obviously implies Cond2, and Cond2 implies Cond1 since for any strategy the opponent adopts, the set of reachable game states is a subset of that when the opponent adopts the null strategy.

Definition 9 Given a BAT D and a complete FSA strategy S for player p, we say S is a winning strategy if the composition C of S and the null strategy satisfies

Note that we only consider games which always ends in a finite number of moves. Thus in the definition, we do not need to require that the strategy must ensure the game ends.

We stress that to verify if an FSA strategy is a winning strategy wrt a BAT D, representing a class of (possibly infinitely many) games, we have a theorem-proving task. Since D includes a second-order induction axiom for situations and T ∗C is a second-order formula, the verification of winning strategies is a second-order reasoning task.

In fact, the winning property of strategies is an example of safety properties, asserting that a formula φ holds in any reachable game state if the strategy is adopted, which can be formalized as follows: D |= ∀q, s.T ∗C (Q0, S0, q, s) ⊃ φ(s).

4 Theoretic Foundations

In this section, we introduce the theoretic foundations for our method for automatic verification of FSA strategies.

We first define the concept of the winning condition of state q for player p. Intuitively, it means the condition that starting from q, whenever the game ends, p wins.

Definition 10 Let C be a composite strategy. The winning condition of state q for player p, written W(p, q, s), is defined as the formula:

The concept of loop invariants plays an important role in program verification. It can be naturally extended to FSA strategies and employed to prove that D |= W(p, Q0, S0).

Thus a complete strategy S is a winning strategy for player p if D |= W(p, Q0, S0).

We will make use of two kinds of labeling of strategy states. The first kind labels each state with a formula, and we call it an F-labeling. The second kind labels each state with a set of small models, and we call it an M-labeling.

Definition 11 Given a BAT D and an FSA composite strategy C, we say an F-labeling X of C is an invariant of C, if for any edge q τ→ q′ , we have

So an invariant of C is a labeling of each state of C with a formula such that if the formula is true in the state, in any successor state, its label formula will also be true.

Definition 12 Given a BAT D, an FSA composite strategy C, and an invariant X of C,

1. we say X is sufficient if for any state q, we have D |= ∀s.X(q)[s] ∧ end(s) ⊃ win(p, s);

Proposition 3 Let X be a sufficient invariant of composite strategy C. Then for any state q, we have D |= ∀s.X(q)[s] ⊃ W(p, q, s). If X is also necessary, then the strategy for p is a winning strategy.

Proof: We prove that for any state q, we have D |= ∀s, q′ , s′ .X(q)[s] ∧ T ∗C (q, s, q′ , s′ ) ∧ end(s′ ) ⊃ win(p, s′ ). Let M be a model of D. We prove that M |= X(q)[s] ∧ T ∗C (q, s, q′ , s′ ) ∧ end(s′ ) ⊃ win(p, s′ ) for any q, s, q′ , s′ . We prove by induction on the distance d between s and s′ . Basis: d = 0 hence q′ = q and s′ = s. By the given condition, we have M |= X(q)[s] ∧ end(s) ⊃ win(p, s). Thus M |= win(p, s). Induction: We assume the proposition holds when d = n, and proceed to prove that it holds when d = n + 1. So suppose M |= X(q)[s] ∧ T ∗C (q, s, q′ , s′ ) ∧ end(s′ ) and dist(s, s′ ) = n + 1. Then there exist q′′ and s′′ such that M |= TC(q, s, q′′ , s′′ ) ∧ T ∗C (q′′ , s′′ , q′ , s′ ) and dist(s′′ , s′ ) = n. By the definition of TC, there is an edge q τ→ q′′ s.t. M |= Do(τ, s, s′′ ). Since X is an invariant, M |= X(q′′ )(s′′ ). Now by induction, M |= win(p, s′ ).

In the following, we first show how to verify if an Flabeling is an invariant by using the idea of regression. Then we will analyze properties of necessary invariants.

Definition 13 Let C be an FSA composite strategy and X an F-labeling of C. The regression of X wrt C, written R(X, C), is a new F-labeling X′ defined as follows: for each state q, X′ (q) = ∧q τ→q′ R(X(q′ ), τ ). By Proposition 2 from Preliminaries, we have

Proposition 4 Let X be an F-labeling of C. If D |= X ⊃ R(X,C), meaning D |= ∀s.X(q)[s] ⊃ R(X,C)(q)[s] for each state q, then X is an invariant of C.

We now extend the notion of small model progression wrt a program to that wrt a strategy.

Definition 14 Let C be an FSA composite strategy and L an M-labeling of C. The progression of L wrt C, written P(L,C), is a new M-labeling defined as follows: for each state q′ , L′ (q′ ) = L(q′ ) ∪ ⋃q τ→q′ prog(L(q), τ).

Definition 15 Let C be an FSA composite strategy and M a small model. We inductively define a sequence Ln, n ≥ 0, of M-labelings as follows:

• L0(q0) = {M}, and L0(q) = ∅ for all state q ̸= q0;

We call Ln the nth progression of M wrt C, and denote it by P n (M, C).

• Ln+1 = P(Ln, C), for n ≥ 0.

Intuitively, M ′ ∈ P n (M, C)(q) iff starting fromM at state q0, by following the strategy for at most n steps, M ′ is a possible model for state q.

Proposition 5 Given a BAT D, let X be a necessary invariant of a composite strategy C. Let M0[S0] |= DS0 , and Ln = P n (M0,C), n ≥ 0. Then for any state q, for any M ∈ Ln(q), M |= X(q).

Proof: We prove by induction on n. Basis: n = 0. Since M0[S0] |= DS0 and DS0 |= X(Q0)[S0], M0 |= X(Q0). Induction: Ln+1 = P(Ln,C). It suffices to prove that for each q τ→ q′ , if M |= X(q), thenM ′ |= X(q′ ), where M ′ = prog(M, τ). Since X is an invariant, D |= ∀s, s′ .X(q)[s] ∧ Do(τ, s, s′ ) ⊃ X(q′ )[s′ ]. Since M[s],M[s′ ] |= Do(τ, s, s′ ), we get if M |=X(q), thenM ′ |=X(q′ ).

In this paper, we consider invariants of the form (end(s) ⊃ win(p, s)) ∧ φ, where φ is a CNF formula whose free variables are implicitly universally quantified. We use counterexample-guided local search for sufficient and necessary invariants. Below, we give the relevant definitions.

A literal is an atom or the negation of an atom. A clause is a set of literals, understood as their disjunction. If a clause has free variables, they are implicitly universally quantified. For example, the clause c : ¬P(x, y) ∨ ¬P(y, z) ∨ P(x, z) is understood as ∀x, y, z.c. The length of a clause c, written |c|, is the number of literals in c. A CNF is the conjunction of clauses. A CNF is considered to have a default clause ⊤.

Definition 16 Let c be a clause, and M+ and M- sets of models. We say that c characterizes M+ vs M- if each model of M+ satisfies c and each model of M- falsifies it.

Definition 17 Let c1 and c2 be two clauses. The distance between c1 and c2 is defined as follows: dist(c1, c2) = max{|c1 - c2|, |c2 - c1|}, where "-" is set difference. Let k be a positive integer. A k-neighbor of a clause c is a clause c′ s.t. their distance is bounded by k.

5 Automatic Verification of FSA Strategies

In this section, we present our method for automatic verification of FSA strategies.

The main idea of our method is as follows. Let S be a complete FSA strategy and C its composition with the null strategy. To prove that S is a winning strategy, we attempt to find a sufficient and necessary invariant X of C. As the initial value of X, we label each state with end(s) ⊃ win(p, s). We check if X is an invariant, i.e., if |= X ⊃ R(X, C). If not, we obtain counterexamples and use them to do a local update of X to exclude the counterexamples. The update may fail. In case of failure, we restart with end(s) ⊃ win(p, s). If X is an invariant, we check if it is necessary, i.e., if DS0 |= X(Q0)[S0]. If so, we return yes. Otherwise, we obtain a counterexample and we compute the nth progression of it wrt C. Now for

Algorithm 1: verify(D, S, p) 1 C := the composition of S with the null strategy 2 Θ := genPreds(D, S) 3 L-,L+ := Label[C, ∅] 4 X := Label[C, end(s) ⊃ win(p, s)] 5 while not timing-out do 6 while ⊭ X ⊃R(X,C) do 7 foreach state q s.t. there is a counterexample Mq of X(q) ⊃ R(X, C)(q) do 8 L(q) := {Mq} 9 update-(X, L, L-, L+) 10 if update- fails then reset(X,L-,L+); 11 if DS0 |=X(Q0)[S0] then return yes ; 12 else 13 M := a counterexample of DS0 ⊃X(Q0)[S0] 14 L := P n (M, C) for a sufficiently large n 15 update+(X, L, L-, L+) 16 return unknown

2 let X(q) = (end(s) ⊃ win(p, s)) ∧ c1 ∧ . . . ∧ cn 3 c′ := a maximal k-neighbor of some ci s.t. c′ characterizes L+(q) versus L-(q)(ci) ∪ L(q) 4 if such a c′ does not exist then return failure ; 5 replace ci in X(q) with c′ 6 L-(c′ )(q) := L-(ci)(q) ∪L(q)

Algorithm 2: update-(X, L, L-, L+) 1 foreach state q s.t. L(q) ̸= ∅ do 7 return success

each state q, we do a local update of X(q) to include the small models associated to q. Then we repeat the process.

Our verification method is presented by Algorithm 1. We first generate from D and S the set of predicates used to form the X labels of states. We make use of two M-labelings of C: for each state q, L-(q) is a set of models that X(q) should exclude, and L+(q) is a set of models that X(q) should include. The X label of each state is in the form of (end(s) ⊃ win(p, s)) ∧ φ, where φ is a CNF. Thus for each state q, L-(q) is actually stored in the form of L-(q)(c) for each clause of X(q), where L-(q)(c) is a set of models that falsify c. As the initial values of L- and L+, we label each state with the empty set. As the initial value of X, we label each state of C with end(s) ⊃ win(p, s). The update- (resp. update+) procedure is presented by Algorithm 2 (resp. 3).

To update the X label of a state, for a clause, we choose a maximal k-neighbour of it. We define a preference relation over clauses so that after reset, we will make choices different from those made earlier. The definition is through a scoring function. Initially, the score of each literal is 0. During reset, we decrease by one the score of each literal appearing in a clause which is replaced since the last reset. The score of a clause is the sum of the scores of the literals in the clause. A clause c1 is preferred over another clause c2 if score(c1) >

Algorithm 3: update+(X, L, L-, L+)

1 foreach state q s.t. L(q) ̸= ∅ do 2 let X(q) = (end(s) ⊃ win(p, s)) ∧ c1 ∧ . . . ∧ cn 3 L+(q) := L+(q) ∪L(q) 4 foreach ci do 5 c′i := a maximal k-neighbor of ci s.t. c′i characterizes L+(q) versus L-(q)(ci) 6 if such a c′i does not exist then 7 c′i := ⊤; L-(q)(ci) := ∅; 8 replace ci in X(q) with c′i

score(c2) or score(c1) = score(c2) and |c1| < |c2|.

We emphasize that our algorithm is deterministic since we do not use randomization: the reason we find different invariants after restart is that when we restart, we update the score function and hence the preference relation between clauses.

Note that in Alg. 1 (Lines 6 and 11), we use the SMT solver Z3 [de Moura and Bjørner, 2008] for checking first-order entailments. If Z3 is unable to decide within the given time, it returns "unknown". In such a case, we will backtrack. If the last update of X occurs in a call to update- (resp. update+), for each state q, we make another choice to update X(q).

Finally, the genPreds process is defined as follows. Extract from the given BAT D and strategy S the set C of constant symbols, set F of function symbols including both situation-independent functions and functional fluents, and set P of predicate symbols. Our basic idea of predicate generation is to generate predicates whose arguments are terms such as P(x) and P(f(x)). However, to control the number of generated predicates, we only generate elementary predicates, that is, predicates of the form t = f(⃗t) or P (⃗t), where f is a function symbol, P is a predicate symbol, and t is a constant or variable. In fact, any predicate can be expressed as a conjunction of elementary predicates, for example, P(f(x)) can be expressed as P(y) ∧ y = f(x). To further control the number of generated predicates, we use at most m ≥ 2 different variables x1, . . . , xm in each generated predicate. We use symmetry and other properties to reduce the number of arithmetic predicates generated, e.g., we generate the predicate x = y + 1 but not x = y + 0 or x = 1 + y.

Clauses are generated as follows: Each clause uses at most n ≥ 3 variables x1, . . . , xn; Atoms are obtained from generated predicates by applying injections from variables into variables. For example, from a generated predicate P(x, y), we can get the clause ¬P (x, y) ∨ ¬P (y, z) ∨ P (x, z).

Example 1 cont'd We extract the following symbols:

P = {turn(p), x > y, x ≥ y, ch(x, y), last(x, y)}. Thus examples of generated predicates are: turn(P1), turn(p), x > 0, x > y, 2 > x, N > 2, ch(x, y), ch(1, 1).

Theorem 1 Given a BAT D and a complete strategy S for player p, when Alg. 1 returns yes, X is a sufficient and necessary invariant, hence S is a winning strategy.

In fact, Algorithm 1 can be easily generalized for verifying safety properties: to verify that a formula φ always holds, we replace end(s) ⊃ win(p, s) in the algorithm with φ(s).

Example 1 cont'd We now illustrate the running process of our algorithm with the strategy shown in Figure 2. We only show the evolution of the label of state q1: After the first call to update-, we get: X(q1) : [¬ch(1, 1) ⊃ turn(P1)] ∧ [¬N > x] After several calls to update- and update+, we have: X(q1) : [¬ch(1, 1) ⊃ turn(P1)] ∧ [¬ch(x, x) ∨ N ̸= x] ∧[0 ≥ x ∨ 0 ≥ y ∨ ¬ch(x, y) ∨ ch(y, x)] Now a counterexample M is generated: {〈ch(1, 1), ch(1, 2), ch(1, 3), ch(1, 4), ch(2, 1), ch(3, 1), ch(4, 1), turn(P2), N = 4〉} Calling update-, we add a new clause [N = x ∨ x ̸= 2]. Now we get a sufficient invariant, but when we check if DS0 |=X(Q0)[S0], we get a counterexample M ′ : {〈ch(1, 1), ch(1, 2), ch(1, 3), ch(2, 1), ch(2, 2), ch(2, 3), ch(3, 1), ch(3, 2), ch(3, 3), N = 3〉} After doing model progression, we have L(q2) : {〈ch(1, 1), ch(1, 2), ch(1, 3), ch(2, 1), ch(3, 1), N =3〉, 〈ch(1, 1), ch(1, 2), ch(2, 1), N =3〉, 〈ch(1, 1), N =3〉} Calling update+, we replace N = x ∨ x ̸= 2 by x ≥ N ∨ 2 ≥ x. ... Finally, we get a sufficient and necessary invariant: X(q1) : [¬ch(1, 1) ⊃ turn(P1)] ∧[0 ≥ x ∨ 0 ≥ y ∨ ¬ch(x, y) ∨ ch(y, x)] ∧[¬ch(x, x) ∨ 2 > x] ∧ [¬last(x, 0)] Thus the given strategy is a winning strategy.

6 Experimental Results

We implemented our algorithm using Python and Z3. All experiments were conducted on a Linux machine with 3.50GHz CPU and 16GB RAM. We set the implementation parameters as follows: The time-out bound for Z3 is 10 second; when updating the X-label, we use 2-neighbors of clauses; when generating predicates we use at most 2 variables and when generating clauses we use at most 4 variables. We did experiments on two types of domains: one from the combinatorial game literature and the other from the generalized planning literature, and we adapt the second type into our framework by adding an agent who is always doing the null action.

The following are two-agent domains and strategies to verify. The domains may look similar in that they all involve placing or removing tokens from finite grids. However, even board games can be very different: difference in game rules or initial settings lead to difference between games. For instance, the winning strategies for Chomp2xN and ChompNxN are quite different, thus the set of reachable sates and hence invariants are different.

PickStone123 (134): There are n stones and two players take turns to remove 1, 2 or 3 (resp. 1, 3 or 4) stones. The one who has no stones to remove loses the game. The strategy for player 1 is to remove stones so that the number of remaining stones satisfies n%4 = 0 (resp. n%7 = 2 ∨ n%7 = 0).

Chomp2xN (NxN): For Chomp2xN, the strategy for player 1 is this: first, eat the cookie in position (2,N); when player 2 eats the cookie in position (1, x) (resp. (2, x)), respond with eating the cookie in position (2, x-1) (resp. (1, x+1)).

Clobber: On a 2xN grid, where N is even, white tokens are placed in the first row, and black ones in the second row. A player moves by using one of his tokens to replace an adjacent token of the opposite colour. The one who has no moves to take loses the game. The strategy for player 2 is: if player 1 removes a token t in the nth column, where n is odd (resp. even), then player 2 removes the token in the (n-1)th (resp. (n + 1)th) column to replace t.

Clobber∗ : The same as Clobber except that player 1 can only remove tokens in the odd columns. The strategy for player 2 is to replace any token that has just replaced her tokens.

Coloring: Two players take turns to paint blue or red on a 1xN grid. Painting red (resp. blue) on a cell is possible if the cell is not painted or painted with blue (resp. red). Painting on a coloured cell turns it into green. The game ends when all cells are colored. Player 1 wins if all cells are green. The strategy for player 2 is: If her opponent paints red (resp. blue) on some cell, then she paints blue (resp. red) on the same cell.

The following are programs in single-agent domains from [Mo et al., 2016]:

1D: Visit all elements in an array from right to left.

Find: Set the ith element of an array inb to true if the ith element of an integer array ina is not 0, and to false otherwise.

Arith: Increase a variable from 0 to 2N.

Sort: Sort an array by using a single loop.

PrizeA1: Visit all the NxN cells through a nested loop.

Add: Increase a variable from 0 to AxB via a nested loop.

Experimental results are summarized in Table 1. Here C is the number of states in the composite strategy, P is the number of generated predicates, U- and U+ denote the total times of calling update- and update+, B and R denote the total times of backtracking and reset, respectively, and T (in seconds) is the total time for verification. Our system successfully verifies all the domains except Clobber. Note that we solve PrizeA1, which cannot be solved by [Mo et al., 2016].

7 RelatedWorks

General game playing [Genesereth et al., 2005] aims at creating a system capable of playing arbitrary games, represented by the Game Description Language (GDL). Some works [Ramanujam and Simon, 2008; Zhang and Thielscher, 2015]

based on PDL (Propositional Dynamic Logic) or GDL concerned about representing and reasoning about the internal structure of strategies. Xiong and Liu [2016] extended the situation calculus for strategy representation and reasoning, and used a simple fragment of Golog for representing structured strategies. However, these works do not consider the representation and automatic verification of general strategies.

There has been some progress on automated reasoning in the situation calculus. Claßen and Lakemeyer [2008] proposed a method to verify temporal properties of nonterminating Golog programs. Based on it, De Giacomo et al. [2010] devised techniques for verification of strategic properties of situation calculus game structures. However, it is unknown whether the fixed-point computation method used in these works can be efficiently implemented. Li and Liu [2015] and Mo et al. [2016] explored automatic verification of partial correctness of Golog programs via discovery of loop invariants. The idea is to start with a sufficient condition and iteratively strengthen it until it becomes an invariant and then check if it is necessary. So they strengthen existing formulas but do not update them when needed as we do. When a discovered invariant is not necessary, their verification simply fails, whereas we continue the search process. Moreover, they do not use counterexamples to guide the discovery process.

De Giacomo et al. [2016a; 2016b] investigated bounded action theories in the situation calculus. A bounded action theory is one which entails that, in every situation, the number of object tuples in the extension of fluents is bounded by a given constant. The verification of a first-order variant of the µ-calculus and the verification of ConGolog programs are decidable for such theories. However, in general, the action theories we consider in this paper are not bounded. For example, even the initial KB of our chomp action theory is not bounded, since there is no bound on the size of the grids.

8 Conclusions

In this paper, we have proposed FSA strategies to represent structured strategies that solve a class of (possibly infinitely many) games with similar structures, and formalized their semantics in the situation calculus. We have proposed a sound but incomplete method for verifying if an FSA strategy is a winning strategy by using counterexample-guided local search for sufficient and necessary invariants. This is a method for verifying safety properties of strategies in general. We implemented our method and experimented with both two-player and single-player domains, and our experiments yielded encouraging results. A limitation of our work is that we consider invariants of the form of a CNF formula where variables are implicitly universally quantified. In the future, we are interested in more expressive invariants which allow existential quantification. More importantly, based on the presented work, we will explore automatic synthesis of FSA strategies via counterexample-guided refinement.

Acknowledgments

We acknowledge support from the Natural Science Foundation of China under Grant No. 61572535.