Model Checking Knowledge in Pursuit Evasion Games

1 Introduction

Pursuit-Evasion games are a type of multi-player game in which one or more pursuers have the objective of identifying the presence of one or more evaders, and of capturing them. Solutions to pursuit-evasion problems have multiple applications, including air and naval combat, ship navigation, [Isaacs, 1965], automatic car collision avoidance systems [Lachner et al., 2000], air traffic control, and unmanned aerial vehicle control [Vidal et al., 2002]. Epistemic model checking is an approach to automated verification, in which one checks whether a model satisfies a formula that describes how the knowledge of agents evolves over time.

Our contribution in this paper is to develop examples of the use of epistemic model checking in pursuit-evasion problems. In particular, we identify specifications requiring the use of the expressiveness provided by epistemic logic, and conduct some experiments in which we apply the model checker MCK [Gammie and van der Meyden, 2004] on some small scale examples. In particular, we compare the performance of two epistemic model checking approaches provided by MCK: BDD based model checking and bounded model checking.

We define the pursuit-evasion games with incomplete information that we study in Section 2. We explain epistemic model checking in Section 3. Section 4 studies the most basic question in pursuit-evasion games - can the pursuers capture an evader - in the context of full-information games. In Section 5, we consider games where the players do not have full

∗ Work supported by Australian Research Council Linkage Grant LP0882961 and Defence Research and Development Canada (Valcartier) contract W7701-082453.

Patrick Maupin

Defence R&D Canada Valcartier, Quebec

Ron van der Meyden

Computer Science and Engineering, University of New South Wales, Australia

visibility: here we argue that epistemic specifications are of particular interest. We discuss related work in Section 6, and conclude with ideas for future work in Section 7.

2 Pursuit-Evasion Games

The pursuit-evasion games we consider in this paper are discrete games with limited visibility in which the agents have complete knowledge of the map, which is represented as a graph, with players able to move to an adjacent node in each step. Our approach involves consideration of a number of different memory assumptions.

More precisely, each game is played on a map M = (V, Em, Ev) where V is a set of vertices (or positions), Em ⊆ V × V is a set of adjacency edges, along which players can move, and Ev ⊆ V × V is a set of edges indicating visibility: a player at position u can see another player at position v just in case (u, v) ∈ Ev. Most of our examples use undirected graphs, so that both relations Em, Ev are symmetric. Generally, we also have that Em is reflexive, so that staying at the same location is a valid move.

A game state on a map M = (V, Em, Ev) consists of a tuple (AP, AE, posn, turn), where AP is a set of pursuers, AE is a set of evaders, posn : AP ∪ AE → V is a function giving the location of each pursuer and evader, and turn ⊆ AP ∪ AE indicates the set of scheduled agents. A game is given by a tuple G = (M, I, sched), where M is a map, I is a set of initial game states on M, and sched is a scheduler, which maps each finite play of the game to a set of agents: the agents that enabled to make a move in the next step. We consider two types of schedulers in this paper. The synchronous scheduler enables all players at all moves, and the turn-based scheduler alternates scheduling of all pursuers with scheduling of all evaders. We consider a variety of game objectives in our examples, so do not include winning conditions in this definition of a game.

A play of the game consists of a finite or infinite sequence s0, s1, . . . where s0 ∈ I, and at each step i, if si = (AP, AE, posn, turn), and si+1 = (A ′ P , A ′ E , posn ′ , turn ′ ), then A ′ P = AP, A ′ E = AE, turn ′ is determined from turn by the scheduler rule sched, and the scheduled agents move across an edge in the adjacency graph, i.e., for each agent a ∈ turn, we have (posn(a), posn ′ (a)) ∈ Em, and for each agent a ∈ (AP ∪ AE) \ turn, we have posn ′ (a) = posn(a).

In each game state, each player a makes an observation of the game state. This is captured by an observation function Oa with domain the set of game states. We define Oa((AP, AE, posn, turn)) = (AP, AE, posna, turn), where posna(b) = posn(b) if player b is either equal to a or visible from player a's position, i,.e., (posn(a), posn(b)) ∈ Ev, and posna(b) = ⊥ otherwise, indicating an unknown position. The player's perfect recall view of a play s0s1 . . . is the sequence of observations viewa(α) = Oa(s0), Oa(s1), . . ..

A strategy for player a is a function σa mapping each possible view α of the player, ending in an observation (AP, AE, posna, turn) where that player is scheduled to move (i.e. a ∈ turn), to a set of positions σa(α) to which that player is able to move, i.e., such that (posna(a), x) ∈ Em for all x ∈ σa(α). Note that the strategy maps to a set of positions in order to allow the strategy to be to make a random move. A strategy assignment is a mapping σ associating a strategy σa to each agent a ∈ AP ∪ AE. A play s0s1 . . . is consistent with a strategy assignment σ if for each player a and each step from si = (AP, AE, posn, turn) to si+1 = (AP, AE, posn ′ , turn ′ ), if a moves in this step (i.e. a ∈ turn) then it moves to one of the positions selected by its strategy (i.e., posn ′ (a) ∈ σa(viewa(s0 . . . si))).

3 Epistemic Model Checking

Model checking [Clarke et al., 1999] is an automated method for formal verification, in which an algorithm is used to check whether a specification expressed in a formal logic holds in a particular model that represents the system to be verified. Model checking is well developed for temporal logic specifications and finite state automata models. Epistemic logic [Fagin et al., 1995] provides a formal language in which one can specify how the information possessed by agents in a distributed or multi-agent system changes over time. In recent years, a number of model checkers have been developed for specifications that combine temporal and epistemic expressiveness [Gammie and van der Meyden, 2004; Lomuscio et al., 2009; Eijck, 2004; Su et al., 2007].

We work in this paper with the epistemic model checker MCK, which supports a specification language that combines operators from the branching time logic CTL ∗ with operators from the logic of knowledge. The fragment relevant to our purposes has syntax given by the following grammar:

where p is an element of the set Prop of atomic propositions and i is an element of the set of agents Agt = AP ∪ AE. Intuitively, Aφ says that φ holds in all possible futures, Xφ says that φ holds at the next moment of time, Gφ says that φ holds now and at all future times, and Kiφ says that agent i knows that φ is true. Other operators that can be defined from this set include Eφ = ¬A¬φ (φ holds in some possible future), and Fφ = ¬G¬φ (φ holds at some future time).

Semantics of the logic can be given using interpreted systems [Fagin et al., 1995]. Let S be a set, which we call the set of environment states. A run over environment states S is a function r : N → S × Πi∈AgtLi, where each Li is some set, called the set of local states of agent i. These local states are used to concretely represent the information on the basis of which agent i computes its knowledge. Given a run r, agent i and time m, we write ri(m) for the corresponding component (in Li) of r(m), and re(m) for the first component (in S ). An interpreted system over environment states S is a tuple I = (R, π), where R is a set of runs over environment states S , and π : R × N → P(Prop) is an interpretation function.

A point of I is a pair (r,m) where r ∈ R and m ∈ N. The semantics of CTL ∗ Kn is given by a relation I, (r,m) |= φ, where I is an intepreted system, (r,m) is a point of I, and φ is a formula, defined inductively as follows (we omit details for the boolean operators):

• I, (r,m) |= p if p ∈ π(r,m),
• I, (r,m) |= Aφ if for all runs r ′ ∈ R with r ′ (k) = r(k) for all k = 0 . . . m, we have I, (r ′ ,m) |= φ,
• I, (r,m) |= Xφ if I, (r,m+ 1) |= φ,
• I, (r,m) |= Gφ if for all times m ′ ≥ m we have I, (r,m ′ ) |= φ,
• I, (r,m) |= Kiφ if for all points (r ′ ,m ′ ) of I such that ri(m) = r ′ i (m ′ ) we have I, (r ′ ,m ′ ) |= φ.

The systems of interest in this paper have runs derived from all plays of a game G, and local states assigned using what MCK call the observational semantics. We allow agents to retain some memory of their past observations, represented by a memory assignment μ that associates to each agent a a function μa mapping perfect recall views of a to some set of memory values. We require that this function have the following Markov property: there exists a function f such that for all views α and observations o, μa(αo) = f (μa(α), o). This permits memory to be incrementally maintained.

Suppose ρ = s0s1 . . . is an infinite play of the game consistent with strategy assignment σ. Given a memory assignment μ, we construct a run r = ρ obs,μ by defining re(m) = sm and ri(m) = (Oi(sm), μi(viewi(s0 . . . sm-1))) for all i ∈ Agt and m ∈ N. That is, each player's local state is its current observation, plus its memory of its previous observations. We write I obs (G, σ, μ) for the system in which the set of runs consists of ρ obs,μ for all infinite plays ρ of G consistent with σ.

The propositions of interest for our analysis are as follows:

• caughte: the evader e has been caught. In case of the turn-based scheduler, this means that for some pursuer p ∈ AP, we have posn(p) = posn(e). When we use the synchronous scheduler, it is possible that a pursuer and an evader traverse an edge in opposite directions in the same step, i.e., posn ′ (p) = posn(e)∧posn ′ (e) = posn(p). In this case, this is also treated as a capture.
• posi ∈ X, where i ∈ Agt and X ⊆ V is a set of game positions. This is true just in case posn(i) ∈ X.

The interpretation π is constructed so as to associate these meanings with these variables.

Given a finite state environment E, and an assignment of protocols P being executed by the agents in this environment, and a formula φ of the logic of knowledge and time, MCK builds an interpreted system I, and checks whether φ holds at time 0 in all runs of I, i.e., whether I, (r, 0) |= φ for all runs r of I. In the applications of interest in the present paper, the environment corresponds to a game G, the assignment of protocols corresponds to the strategy assignment σ, and the system I is I obs (G, σ, μ) for some memory assignment μ.

MCK supports several different algorithmic approaches for solving the model checking problem. We use two in the present paper: 1) Ordered binary decision diagram (BDD) based model checking, (MCK's algorithms spec obs ctl and spec obs ctls) and 2) Bounded model checking (BMC) (MCK's algorithm spec obs bmc), which is based on translation to a propositional logic satisfiability problem and works on the universal fragments of the logic by finding a counterexample in case the specification fails. MCK supports diagnosis by listing and visualization of counterexamples.

In the following sections, we present examples of the application of epistemic model checking using MCK where the system is a pursuit-evasion game. Our focus is to identify epistemic specifications of interest in this domain, and to obtain some preliminary results on the performance of MCK on these examples. The experiments were conducted on an Apple iMac with a 3.06GHz Intel i3 processor and 4G memory.

4 Pursuit Verification

The first example models a full-information pursuit-evasion game where the arena is a (m×n)-grid, and two pursuers chase an evader. In a full-information game, agents can observe the whole system, Thus, the map M = (V, Em, Ev) is given by V = [0 . . .m - 1] × [0 . . . n - 1], Em = {((x, y), (x ′ , y ′ )) ∈ V 2 | (x = x ′ ∨ y = y ′ ) ∧ |x - x ′ | ≤ 1 ∧ |y - y ′ | ≤ 1} and Ev = V × V. Figure 1 presents the case of a (5 × 5)-grid. The evader is initialized at position (0, 0) and the pursuers are initialized at position (4, 0) and (0, 4), respectively.

We consider two variants of the game, with strategies depending on the type of scheduler used. The strategy of the evader is always to move randomly to an adjacent vertex.

• synchronous scheduling: The pursuers choose any move in the direction of the current evader position.
• turn-based: The pursuers execute a pincer movement: one prioritizes moving towards the horizontal position of the evader, the other prioritizes the vertical. Once horizontally/vertically aligned, the pursuer may move towards the evader in the other dimension.

The point of these examples is to demonstrate some basic pursuit issues: is it possible for the evader to avoid capture when the pursuers are following the particular strategy prescribed for them? Thus, the formula

expresses that the evader cannot avoid capture (on all paths there exists a future time where the evader has been caught).

We may model check this using BDD-based model checking. Alternately, since this is a universal formula, we may also use bounded model checking. In this case, if the formula is false and a large enough bound N is selected, then the model checker returns a counterexample trace that satisfies G¬caughte, i.e. on which the evader avoids capture.

In the turn-based game, model checking verifies that capture is guaranteed. However, in the synchronous game, the specification fails to hold: the evader can escape capture if the pursuers choose their moves poorly. The counterexample facilities can be used to investigate the failure, and reveal the following pattern of movement in which the evader avoids capture in a loop such as ((1, 2), (0, 1), (2, 1)) → ((1, 1), (0, 2), (2, 2)) → ((1, 2), (0, 1), (2, 1)) with the triples (posn(e), posn(p1), posn(p2)) denoting the positions of evader and pursuers.

The experimental results for model checking specification (1) in the grid game are shown in Figure 2, which gives a logscale plot of model checking runtime against the grid dimension n for an n × n grid. The specification is false in the synchronous case, and we also plot the counter-example size in number of steps: this turns out to be roughly half the grid size plus 4. Timing results are omitted in the case of BMC and the turn-based game, since there exists no counterexample to be found, so the BMC approach does not terminate (MCK does not attempt to determine a sufficient bound for termination of BMC). In this example, as we increase the problem size, the BMC-based model checking scales well, while BDD model checking runtime becomes large (we terminated the computation at 2 hours) at thresholds that appear to be related to an increase in the number of bits required to represent the dimension.

Note that this analysis uses temporal specifications only, so any temporal logic model checker could be used to do the same analysis. The main point of these examples is to check how the two algorithm types compare and how well the epistemic model checker MCK runs as we scale the examples. It appears the approach is feasible for moderate sized examples.

5 Region Clearing and Pursuit Verification

We now consider some examples where the agents do not have complete visibility, and some game objectives become of interest, for which epistemic model checking is required, since temporal model checking does not suffice.

In all the games in this section, a single pursuer chases a single evader, and scheduling is turn-based. The map in these examples is based on variants of the undirected movement graph (V, Em) depicted in Figure 3. (We explain the dotted edges below.) Initially, the pursuer is at position 1, and the evader can be at any position, including a special position 0, which indicates that the pursuer is not present in the game. Let Q be the set of all positions other than 0.

The visibility graph in the examples is derived from Figure 3 by (u, v) ∈ Ev if u and v are connected in the figure by a sequence of edges forming a straight line (e.g., we have (3, 9), (8, 12) ∈ Ev, but (3, 11), (5, 8) nelement Ev).

In these examples, the evader's strategy is to move randomly through the graph, and we define a particular strategy for the pursuer, to be verified for correctness. The pursuer's strategy is defined in two parts, corresponding to two game objectives: first, to determine whether the evader is present in the region Q, and, second, to capture the evader once it is known to be present. The first part of the strategy is constructed so that the pursuer moves along a prescribed surveillance route, until the evader is seen. At this point the strategy switches to the second part, in which the pursuer gives chase by moving, at each turn, towards the location where it last saw the evader. For example, suppose the pursuer is at position 1, it sees the evader is at position 8, and it is the evader's turn to move. If the evader moves to position 12 it is no longer in view of the pursuer, so the pursuer's move would be to position 4, in the direction it last saw the evader.

In this set of examples, the memory assignment for the evader is the null function, and the memory assignment for the pursuer always retains the position where the evader was last seen (else ⊥) and a boolean variable indicating whether the evader has been caught, plus any additional values described below.

5.1 Version 1: Catch or Clear

In this version of the example the pursuer can both clear the region and capture the evader if present. We drop from the map the position 19 and the edges connected to it. The prescribed surveillance route is 1-4-5-4-8-9-8-12-13-12-16.

This example helps to illustrate the usefulness of epistemic specifications in a situation with partial observability. Since the evader may or may not be in the arena, the pursuer would like to sweep the arena to determine if the evader is present in the arena, and to catch it if so. This objective can be expressed by the specification

which states that the pursuer is guaranteed to eventually capture the evader, or else know that the evader is not in the arena. Alternately, if we do not require capture, but merely that the pursuer knows whether the evader is in the arena, then we could check

Note that it would not suffice to write the purely temporal specification AF(caughte ∨ pose nelement Q). While this does imply that the evader is caught whenever it is present, it does not imply that the pursuer can terminate the search. Possibly the evader is not in Q but the pursuer will never know this fact.

In this version of the game, the pursuer is guaranteed to either clear the region or capture the evader. Model checking confirms that Specifications (2) and (3) both hold. Table 1 lists the experimental results for the BDD-based model checker. The BMC model checker is not included because it is nonterminating for a specification that holds.

5.2 Version 2: Detecting Evadability

We next consider a version where the region can be cleared, but capture is not guaranteed. In this variant, we include position 19 and the edges from it to position 2 and position 3. Since now the evader may be hiding at position 19, not visible from position 1, we adapt the prescribed surveillance route for the pursuer to 1-3-1-4-5-4-8-9-8-12-13-12-16, where we precede the previous route by a move to position 3, where position 19 is visible. In this scenario, the pursuer is able to clear the region, but there exists an infinite chase, in which the pursuer and the evader both move in the same direction along the cycle 1-2-19-3-1. Specification (2) becomes false, but (3) continues to hold.

The bounded model checker can be used to find a counterexample for the specification (2), although it is much slower than BDD-based model checker because of the length of the counterexample.

In this scenario, it is of interest for the pursuer, when it knows that the evader is in the arena, to determine if it is possible for the evader to evade capture. The formula

says that the pursuer is guaranteed to learn whether the evader is in the region, and if it is in the arena, the pursuer will either capture the evader, or eventually know that the evader can (in some cases) evade capture. An arguably clearer, but equivalent, formulation of this is

However, the temporal operators here are not in CTL so it runs a little slower. Experimental results are shown in Table 1.

5.3 Version 3: Capture with Assistance

In the previous version, the pursuer can discover that although the evader is present, it may be able to avoid capture. To address this, the pursuer may call in assistance with the chase. We model this by adding to the map a new position 20, where the assistant waits until it is called, as well as a unidirectional edge from position 20 to position 1. The pursuer calls the assistant at its first turn where it has last seen the evader at one of the positions on the loop where an infinite pursuit may happen, i.e., 1,2,3 or 19. We add a new variable to the pursuer's memory, which records whether it has called for assistance.

The assistant follows a prescribed strategy to help the pursuer catch the evader. It has been waiting for the call at a special position 20. Once called, it moves to position 1 at its next turn. It then moves along the loop 1-2-19-3 in clockwise direction. The pursuer, after calling for assistance, moves towards the loop and then around it in anti-clockwise direction.

In this scenario, the formula (2) holds, as does formula (3). Note that (4) and (5) hold trivially when (2) holds.

6 RelatedWork

The games we have studied in this paper are a special case of motion and sensing problems, which [Isler, 2004] groups into sensor assignment, sensor placement, exploration, and pursuit-evasion. These four problems can be seen as special cases of a more general problem, involving either single or multiple sensors, static or mobile sensors, and a search goal that is either punctual or distributed across the environment. This paper deals primarily with pursuit-evasion games, and the closely related problem of exploration (termed environment clearing above), but we believe epistemic model checking may also be applicable to other problems in this area.

Depending on the scientific community many synonyms are used for somewhat similar problems: art gallery problems in computational geometry [Chv`atal, 1975], [BjorlingSachs and Souvaine, 1995], graph searching in computer science [Megiddo et al., 1988], [Goldstein and Reingold, 1995] and [Gal, 2005], rendezvous problems in operations research [Lim, 1997], [Alpern and Lim, 1998] and [Alpern, 2002], and differential games in control theory [Isaacs, 1965].

The literature on pursuit-evasion games studies a range of models and issues. One of the objectives is to develop general strategies for a class of games, to prove their correctness and analyze their efficiency. For example, [Adler et al.,

2004] provides bounds on expected time to capture for randomized pursuit-evasion protocols for graphs involving one pursuer and one evader. Here neither agent has visibility of the neighboring nodes. The scheduler is synchronous. Isler [Isler, 2004] studies expected time to capture for agents with local visibility of nodes adjacent to their location. He considers reactive evaders, which only move when they see a pursuer, as well as algorithms for classifying graphs according to whether they admit a winning strategy. Other important results are found in [Gal, 2005], [Megiddo et al., 1988] and [Alpern, 1995; 2002].

Our work in this paper differs from the above in that we are interested in obtaining a formal verification of the correctness of a strategy in a particular game, rather than in a class of games. This may be useful even when applied to games for which a theoretical analysis exists, since theoretical proofs are sometimes flawed. Further, a strategy that is asymptotically optimal for a class of games may not be optimal for a specific game in that class, leading mission planners to deviate from the theoretical strategy, so that the proof guarantees no longer apply.

Another benefit of a model checking approach is that we can flexibly handle a larger range of game models than studied in the theoretical literature, investigating questions such as how a game is impacted by changes in the sensor models, player capabilities or game objectives. Such changes may invalidate a theoretical analysis, requiring a lengthy and laborintensive intellectual effort to develop the theory in the new setting. On the other hand, model checking promises to provide an efficient, automated approach to the analysis of particular variants of interest.

A knowledge-based approach to incomplete-information robot motion planning problems is proposed in [Brafman et al., 1997], and one of the examples from this paper has been studied using MCK [Gammie and van der Meyden, 2004]. Model checking based on the interpreted systems model for uncertainty, as a general solution procedure to situation analysis problems in the military domain, has been proposed in [Maupin and Jousselme, 2005] and [Maupin et al., 2010]. So far as we know, our work in this paper is the first detailed study of the application of an epistemic model checker to pursuit-evasion games.

However, others have investigated model checking of specifications in temporal logic as an approach to the analysis of pursuit-evasion games. [Bohn, 2004] uses the symbolic model checker SMV to synthesize a strategy for a pursuer to capture an evader when possible. The grid scenario in this work is different from ours in that the pursuer and evader observe only their current positions and the pursuer has a speed advantage over the evader. The pursuer's knowledge is implicitly encoded in the model with a boolean variable occupiedx for every position x, denoting that the pursuer considers it possible that the evader is at position x. Since this encoding is done by hand, the approach is likely to be difficult to follow in more complex examples, and it leaves the possibility of human error. By comparison, our epistemic model checking approach automates such reasoning about knowledge. [Sirigineedi et al., 2009] uses SMV to check the behavior of a UAV performing a cooperative search mission.

In [Moulin et al., 2003], a bounded model checker is used to check several universal properties in maneuvering target tracking in a planar air-to-air scenario.

7 Conclusion

Our objective in this paper was to clarify the ways that epistemic model checking might be beneficial for the analysis of pursuit-evasion games, and to conduct a number of case studies of small scale in order to confirm its relevance and feasibility. We feel that the results are promising and justify the development of more realistic, larger scale case studies. Encoding of the examples as MCK input scripts was done by hand, and larger scale studies will require tools for automatic generation of model checker input from geographic information systems. We presently have such tools under development and hope to report results in the near future.

Several other directions would be interesting to pursue in future research. We have identified knowledge conditions of interest in the pursuit-evasion setting. Determining explicitly the exact conditions under which an agent has this knowledge would be useful, e.g. for terminating a search or calling in assistance at the earliest possible time. It would also be interesting to develop automated approaches for the synthesis of player strategies in these games, and to apply our approach to strategies from the existing theoretical literature.