A Logical Account of Causal and Topological Maps

1 Introduction

The problem of map building -how an agent creates a discrete spatial representation from its continuous interactions with the environment- can be stated formally as an abduction task where the actions and observations of the agent are explained by connectivity relations among places in the environment [Shanahan, 1996, Shanahan, 1997, Remolina and Kuipers, 1998]. In this paper we consider the Spatial Semantic Hierarchy (SSH) [Kuipers, 2000, Kuipers and Byun, 1988, Kuipers and Byun, 1991] as the agent's target spatial representation. The SSH is a set of distinct representations for large scale space, each with its own ontology and each abstracted from the levels below it. The SSH describes the different states of knowledge that an agent uses in order to organize its sensorimotor experiences and create a spatial representation (i.e. a map). Using the SSH representation, navigation among places is not dependent on the accuracy, or even the existence, of metrical knowledge of the environment.

A3 This work has taken place in the Intelligent Robotics Lab at the Artificial Intelligence Laboratory, The University of Texas at Austin. Research of the Intelligent Robotics lab is supported in part by NSF grants IRI-9504138 and CDA 9617327, and by funding from Tivoli Corporation.

In order to define the preferred models associated with the experiences of the agent, we use a circumscriptive theory to specify the SSH's (minimal) models. Different models can exist that explain the same set of experiences. This occurs because the agent could associate the same sensory description to different environment states, or because the agent has not completely explored the environment. The different SSH levels assume different spatial properties about the environment and the actions performed by the agent. These spatial properties play the role of "filters" the agent applies in order to distinguish the different environment states it has visited. For instance, at the SSH causal level two environment states are considered the same if any sequence of actions started at these states renders the same sequence of observations. At the SSH topological level, two environment states are considered the same if they are at the same place along the same paths. Finally, at the SSH metrical level, two environment states are the same, if it is possible to assign to them the same coordinates in any frame of reference available to the agent. In sections 3 and 4 we make precise the claims above.

Finally, we use the SSH circumscriptive theory as the specification for a logic program used to implement the abduction task. In the paper we provide the logic program for the SSH causal level theory and illustrate how to encode the minimality condition associated with this theory. We have implemented the program using Smodels [Niemel¨ a and Simons, 1997] and confirm that the theory yields the intended models.

2 RelatedWork

The SSH grew out of the TOUR model proposed in [Kuipers, 1977, Kuipers, 1978]. Other computational theories of the cognitive map have been proposed: [Kortenkamp et al., 1995, McDermott and Davis, 1984, Leiser and Zilbershatz, 1989, Yeap, 1988]. These theories share the same basic principles: the use of multiple frames of reference, qualitative representation of metrical information, and connectivity relations among landmarks. They differ in how they define what a landmark is, or the description (view, local 2D geometry) associated with a landmark. Except for McDermott and Davis, none of the theories above has a formal account like the one presented in this paper for the SSH.

Considering map building as a formal abduction task has been proposed by Shanahan [Shanahan, 1996, Shanahan, 1997]. He proposes a logic-based framework (based on the circumscriptive event calculus) in which a robot constructs a model of the world through an abductive process whereby sensor data is explained by hypothesizing the existence, locations, and shapes of objects. In Shanahan's work, space is considered a real-valued coordinate system. As pointed out in [Shanahan, 1997], a problem of Shanahan's approach is the existence of many minimal models (maps) that explain the agent's experiences. We have alleviated this problem by considering the SSH topological map instead of an Euclidean space as the agent's target spatial representation.

The problem of distinguishing environment states by outputs (views) and inputs (actions) has been studied in the framework of automata theory [Basye et al., 1995]. In this framework, the problemwe address here is the one of finding the smallest automaton (w.r.t. the number of states) consistent with a given set of input/output pairs. Without any particular assumptions about the environment or the agent's perceptual abilities, the problem of finding this smallest automaton is NP-complete [Basye et al., 1995].

The SSH [Kuipers, 2000, Kuipers and Byun, 1988, Kuipers and Byun, 1991] abstracts the structure of an agent's spatial knowledge in a way that is relatively independent of its sensorimotor apparatus and the environment within which it moves. At the SSH control level, the agent and its environment are modeled as continuous dynamical systems whose equilibrium points are abstracted to a discrete set of distinctive states. A distinctive state has associated a view describing the sensory input obtained at that distinctive state. The control laws, whose executions define trajectories linking these distinctive states, are abstracted to actions, giving a discrete causal graph representation for the state space. The causal graph of states and actions can in turn be abstracted to a topological network of places, paths and regions (i.e. the topological map). Local metrical models, such as occupancy grids, of neighborhoods of places and paths can then be built on the framework of the topological network while avoiding global metrical consistency problems. In the next sections we formally describe the SSH causal and topological levels.

3 SSH Causal level

We use a first order sorted language in order to describe the SSH causal level. The sorts of this language include distinctive states, views, actions and schemas. The sort of distinctive states corresponds to the names given by the agent to the fixpoints of hill-climbing control strategies. It is possible for the agent to associate different distinctive state names with the same environment state. This is the case since the agent might not know at which of several environment states it is currently located. A distinctive state has an associated view. We use the predicate CE CXCTDBB4CSD7BN DAB5 to represent the fact that v is a view associated with distinctive state CSD7. We assume that a distinctive state has a unique view. However, we do not assume that views uniquely determine distinctive states (i.e. CE CXCTDBB4CSD7BN DAB5 CM CE CXCTDBB4CSD7 BC BN DAB5 BIAX CSD7 BP CSD7 BC ). This is the case since the sensory capabilities of an agent may not be sufficient to distinguish distinctive states.

An action has a unique type, either travel or turn, associated with it. We use the predicate BTCRD8CXD3D2 D8DDD4CTB4CPBN D8DDD4CTB5

to represent the fact that the type of action a is type. Turn actions have associated a unique turn description, either turnLeft, turnRight or turnAround. We use the predicate CCD9D6D2 CSCTD7CRB4CPBN CSCTD7CRB5 to indicate that desc is the turn description associated with the turn action a.

A schema represents an action execution performed by the agent in the environment. An action execution is characterized in terms of the distinctive states the agent was at before and after the action was performed. 1 We use the predicate BVCBB4D7BN CSD7BN CPBN CSD7 BC B5 to denote the fact that according to schema D7, action CP was performed starting at distinctive state CSD7 and ending at distinctive state CSD7 BC . While schemas are explicit objects of our theory, most of the time it is convenient to leave them implicit. We introduce the following convenient notation:

Example 1

Consider a robot moving in the environment depicted in figure 1. The robot moves from distinctive state a to distinctive state b by performing a follow-midline action, ml. Then the robot performs the same action to move to distinctive state c. We assume that all corridor intersections look alike (DAB7). This set of experiences can be described by the formulae:

BTCRD8CXD3D2 D8DDD4CTB4D1D0BN D8D6CPDACTD0B5 BN BVCBB4D7BDBN CPBND1D0BN CQB5 BN BVCBB4D7BEBN CQBND1D0BN CRB5 BN CE CXCTDBB4CPBN DAB7B5 BN CE CXCTDBB4CQBN DAB7B5 BN CE CXCTDBB4CRBN DAB7B5 BM

Given this set of experiences, at the SSH causal level distinctive states a, b and c are not distinguishable. Any known sequence of actions renders the same set of views. However, at the SSH topological level all these distinctive states are distinguishable since the robot has traveled from a to b and then to c following the same path (see example 3). Should the robot continue the exploration and visit distinctive state CS, with view BP, then by relying just on known actions and views the agent can distinguish all distinctive states it has visited (see example 2). CUend of exampleCV

The agent's experiences in the environment are described in terms of CS, View, Action type and Turn desc atomic formulae. Hereafter we use E to denote a particular agent's experience formulae. By CBB4BXB5 we denote the formulae stating that the sorts of schemas, distinctive states, views and actions are completely defined by the sets of schema, distinctive states, view and action constant symbols occurring in E respectively. 2 By BWCC we denote our domain theory, the formulae stating that: (-) the sets CUturn, travelCV, CUturnLeft,turnRight,turnAroundCV, completely define the sorts of action types and turn descriptions; (-) an action has associated a unique action type ; (-) distinctive states have associated a unique view; (-) the description associated with an action is unique; (-) turn actions have associated a turn description; (-) the type of actions as well as the qualitative description of turn actions is the one specified in E. The SSH causal theory CT(E) defines when two distinctive states are indistinguishable at the SSH causal level. We use the predicate CRCTD5B4CSD7BN CSD7 BC B5 to denote this fact. We will assume that actions are deterministic: 3

1 An action execution also has metrical information associated with it. This metrical information represents an estimate of, for example, the distance or the angle between the distinctive states associated with the action execution.

CT(E) is the following nested abnormality theory [Lifschitz, 1995]:

BVCCB4BXB5 BP BXBN CBB4BXB5BN BWCCBN BTDCCXD3D1BDBN BVBX CQD0D3CRCZ

where CEQ block is defined as

CU D1CPDC CRCTD5 BM CRCTD5B4CSD7BN CSD7 BC B5 AX CRCTD5B4CSD7 BC BN CSD7B5BN CRCTD5B4CSD7BN CSD7 BC B5 CM CRCTD5B4CSD7 BC BN CSD7 BCBC B5 AX CRCTD5B4CSD7BN CSD7 BCBC B5BN CRCTD5B4CSD7BN CSD7 BC B5 AX CE CXCTDBB4CSD7BN DAB5 AH CE CXCTDBB4CSD7 BC BN DAB5BN (2) CRCTD5B4CSD7 BD BN CSD7 BE B5CMCWCSD7 BD BN CPBN CSD7 BC BD CXCMCWCSD7 BE BN CPBN CSD7 BC BE CXAXCRCTD5B4CSD7 BC BD BN CSD7 BC BE B5(3) CV

It can be proved that the predicate ceq defines an equivalence relation on the sort of distinctive states. Axiom 2 states that indistinguishable distinctive states have the same view. Axiom 3 states that if distinctive states CSD7 and CSD7 BC are indistinguishable and action a has been performed for both CSD7 and CSD7 BC , then the action links these states with indistinguishable states. By maximizing CRCTD5 we identify distinctive states that cannot be distinguished by actions and/or views, and thereby minimize the set of states represented by the model.

Axioms 2 and 3 allow us to prove the following useful lemma:

Lemma 1 Let BT denote a sequence of action symbols. Let BTB4CSD7B5 denote the distinctive state symbol resulting of starting the sequence BT at distinctive state CSD7 or BR if BT is not defined for CSD7. 4 Then,

CRCTD5B4CSD7BN CSD7 BC B5 CMBTB4CSD7B5 BIBPBR CMBTB4CSD7 BC B5 BIBPBR AX CE CXCTDBB4BTB4CSD7B5BN DAB5 AH CE CXCTDBB4BTB4CSD7 BC B5BN DAB5 BM

Example 2

2 That D7D3D6D8 is completely defined by the constant symbols D7 BD BN BM BM BM BN D7 D2 means that an interpretation for D7D3D6D8 is the Herbrand interpretation defined by the set CUD7 BD BN BM BM BM BN D7 D2 CV.

3 Throughout this paper we assume that formulas are universally quantified.

4 Given an action symbol BT and distinctive state CSD7, BTB4CSD7B5 BP CSD7 BC if the schema CWCSD7BN BTBN CSD7 BC CX has been observed, otherwise, BTB4CSD7B5 BPBR. Moreover,BTB4BRB5 BPBR. The definition is then extended to action sequences in the standard way. Notice that BTB4CSD7B5 being well-defined relies on our assumption that actions are deterministic (Axiom 1).

Consider the situation depicted in Figure 1b, with the corresponding schemas and views as in example 1. Using lemma 1 one can conclude that all distinctive states a, b and c are distinguishable by actions and views alone. For instance, CUD1D0BND1D0CVB4CPB5 BP CR, CUD1D0BND1D0CVB4CQB5 BP CS, CE CXCTDBB4CUD1D0BND1D0CVB4CPB5BN DAB7B5, CE CXCTDBB4CUD1D0BND1D0CVB4CQB5BNBPB5, and consequently, BMCRCTD5B4CPBN CQB5. CUend of exampleCV

The Herbrand models of BVCC B4BXB5 are in a one to one correspondence with the answer sets [Gelfond and Lifschitz, 1991] of the logic program in Figure 2. 5 In this program, the CG and CH variables range over distinctive states and the variable CE ranges over views in BX. The sets of rules 4 and 5 are the facts corresponding to the agent's experiences. Rules 6-8 require CRCTD5 to be an equivalence class. Rules 8 and 9 are the counterpart of axiom 2. Rule 11 is the counterpart of axiom 3. In order to define the maximality condition of CRCTD5, the auxiliar predicate D4B4CGBN CHBN CGBDBN CH BDB5 is introduced. This predicate reads as "If CG and CH were the same, then CGBD and CH BD would be the same". The predicate CSCXD7D8B4CGBN CH B5 defines when distinctive states CG and CH are distinguishable. Constraint 12 establishes the maximality condition on CRCTD5: CRCTD5B4CGBN CH B5 should be the case unless CG and CH are distinguishable. 6

CUCRD7B4CSD7BN CPBN CSD7 BC B5 AW BM BM CRD7B4CSD7BN CPBN CSD7 BC B5 BE BXCV (4) CUDACXCTDBB4CSD7BN DAB5 AW BM BM DACXCTDBB4CSD7BN DAB5 BE BXCV (5) CRCTD5B4CGBN CH B5BNBMCRCTD5B4CGBN CH B5 AW BM D4B4CGBN CHBN CGBN CH B5 AW BM D4B4CGBN CHBN CGBEBN CH BDB5 AW D4B4CGBN CHBN CGBDBN CH BDB5BN CRCTD5B4CGBDBN CGBEB5BM D4B4CGBN CHBN CGBDBN CH BEB5 AW D4B4CGBN CHBN CGBDBN CH BDB5BN CRCTD5B4CH BDBN CH BEB5BM D4B4CGBN CHBN CGBEBN CH BEB5 AW D4B4CGBN CHBN CGBDBN CH BDB5BN CRD7B4CGBDBN BTBN CGBEB5BN CRD7B4CH BDBN BTBN CH BEB5BM D4B4CGBN CHBN CH BDBN CGBDB5 AW D4B4CGBN CHBN CGBDBN CH BDB5BM D4B4CGBN CHBN CGBDBN CH BEB5 AW D4B4CGBN CHBN CGBDBN CH BDB5BN D4B4CGBN CHBN CH BDBN CH BEB5BM CSCXD7D8B4CGBN CH B5 AW D4B4CGBN CHBN CGBDBN CH BDB5BN DACXCTDBB4CGBDBN CE B5BN D2D3D8 DACXCTDBB4CH BDBN CE B5BM CSCXD7D8B4CGBN CH B5 AW D4B4CGBN CHBN CGBDBN CH BDB5BN D2D3D8 DACXCTDBB4CGBDBN CE B5BN DACXCTDBB4CH BDBN CE B5BM AW D2D3D8 CRCTD5B4CGBN CGB5BM (6) AW CRCTD5B4CGBN CH B5BN D2D3D8 CRCTD5B4CHBN CGB5BM (7) AW CRCTD5B4CGBN CH B5BN CRCTD5B4CHBN CIB5BN D2D3D8 CRCTD5B4CGBN CIB5BM (8) AW CRCTD5B4CGBN CH B5BN DACXCTDBB4CGBN CE B5BN D2D3D8 DACXCTDBB4CHBN CE B5BM (9) AW CRCTD5B4CGBN CH B5BN D2D3D8 DACXCTDBB4CGBN CE B5BN DACXCTDBB4CHBN CE B5BM (10) AW D2D3D8 CRCTD5B4CGBDBN CH BDB5BN CRCTD5B4CGBN CH B5BN CRD7B4CGBN BTBN CGBDB5BN CRD7B4CHBN BTBN CH BDB5BM (11) AW D2D3D8 CRCTD5B4CGBN CH B5BN D2D3D8 CSCXD7D8B4CGBN CH B5BM (12)

5 See extended version of this paper [Remolina and Kuipers, 2001] for a proof.

6 We have implemented this logic program in Smodels [Niemel¨ a and Simons, 1997]. In the implementation, one has to add variable domain restrictions to the different rules. For example, rule

becomes

CRCTD5B4CGBN CH B5BN BMCRCTD5B4CGBN CH B5 AW CSD7D8CPD8CTB4CGB5BN CSD7D8CPD8CTB4CH B5

where CSD7D8CPD8CT is our predicate to identify the sort of distinctive states.

4 SSH Topological Level

We are to define the SSH topological theory, CCCCB4BXB5, associated with a set of experiences BX. The language of this theory is a sorted language with sorts for places, paths and path directions. 7 The main purpose of CCCCB4BXB5 is to minimize the set of paths and places consistent with the given experiences BX. A place can be a topological place (hereafter place) or a region. A place is a set of distinctive states linked by turn actions. A region is a set of places. We use the predicates tplace and is region to identify these subsorts. A path defines an order relation among places connected by travel with no turn actions. They play the role of streets in a city layout. We use the predicate tpath to identify the sort of paths. By minimizing the extent of D8D4D0CPCRCT, CXD7 D6CTCVCXD3D2 and D8D4CPD8CW we minimize the sort of places and paths respectively. 8 The language of the SSH topological level includes the following other predicates: teq(ds,ds') - distinctive states CSD7 and CSD7 BC are topologically indistinguishable; at(ds,p) - distinctive state CSD7 is at place D4; along(ds,pa,dir) -distinctive state CSD7 is along path D4CP in direction CSCXD6; OnPath(pa,p) -place D4 is on path D4CP; PO(pa,dir,p,q) -place D4 is before place D5 when facing direction CSCXD6 on path D4CP (PO stands for Path Order).

TT(E), is the following nested abnormality theory:

BKD4BN D8D4D0CPCRCTB4D4B5 AH BMCXD7 D6CTCVCXD3D2B4D4B5 BN BKD4CPBN D8D4CPD8CWB4D4CPB5 BN (13) CUD1CXD2 CXD7 D6CTCVCXD3D2 BM BVCCB4BXB5 BN CC CQD0D3CRCZ BN BTCC CQD0D3CRCZ CV

The first line in Axioms 13 says that topological places and regions are the two subsorts of places, and that the predicate D8D4CPD8CW represents the sort of paths. The block CT(E) is the one defined in the previous section. The block T block defines the predicates CS D8D9D6D2, CS D8D6CPDACTD0, and DI D8D6CPDACTD0 such that CS D8D9D6D2 is the equivalence closure of the schemas CWA1 BN D8D9D6D2BN A1CX; CS D8D6CPDACTD0 and DI D8D6CPDACTD0 are the equivalence and transitive closure of the schemas CWA1 BN D8D6CPDACTD0BN A1CX.

The block AT block (Figure 3) is the heart of our theory. 9 The purpose of this block is to define the extent of the predicates tpath, tplace, at, along, PO and teq, while identifying a minimum set of places and paths that explain BX. The block has associated the circumscription policy 10

circ D8D4CPD8CW AV CPD0D3D2CV AV  AV D2 CPD8CW AV D8D4D0CPCRCT var DI CBCBD4D6CTCS where DI

CBCBD4D6CTCS stands for the tuple of predicates at, teq, travel eq, and turn eq. 11 This circumscription policy states

7 The sort of directions is completely defined by the symbols pos and neg.

8 Notice that our logic has sorts for places and paths but in order to minimize these sorts we have to explicitly have predicates representing them.

9 Notice that the predicate CXD7 D6CTCVCXD3D2 is not mentioned in the theory of figure 3. In the next section we will add to this theory axioms dealing with regions. For the purpose of this section, the minimization of CXD7 D6CTCVCXD3D2 in conjunction with BKD4BN D8D4D0CPCRCTB4D4B5 AH BMCXD7 D6CTCVCXD3D2B4D4B5 implies (the default) BKD4 D8D4D0CPCRCTB4D4B5.

10 The symbol AV indicates prioritized circumscription (see [Lifschitz, 1994] section 7.2).

11 Block 19 in Figure 3 states that the predicate D8D9D6D2 CTD5 corresponds to the relation CS D8D9D6D2 modulo D8CTD5. Block 31 defines D8D6CPDACTD0 CTD5 to be the relation CS D8D6CPDACTD0 modulo D8CTD5.

(among others) that a minimum set of paths is preferred over a minimum set of places. Next we discuss the axioms in AT block.

CU BM D8CTD5B4CSD7BN CSD7 BC B5 AH BLD4 A8 CRCTD5B4CSD7BN CSD7 BC B5 CM CPD8B4CSD7BN D4B5 CM CPD8B4CSD7 BC BN D4B5 A9 BN (14) CPD8B4CSD7BN D4B5 AX D8D4D0CPCRCTB4D4B5BN (15) BLAXD4 CPD8B4CSD7BN D4B5BN (16) CWCSD7BN D8D9D6D2BN CSD7 BC CX CM CPD8B4CSD7BN D4B5 AX CPD8B4CSD7 BC BN D4B5BN (17) CPD8B4CSD7BN D4B5 CM CPD8B4CSD7 BC BN D4B5 AX D8D9D6D2 CTD5B4CSD7BN CSD7 BC B5BN (18) CUD1CXD2 D8D9D6D2 CTD5 BM (19) D8CTD5B4CSD7BN CSD7 BC B5 CM D8CTD5B4CSD6BN CSD6 BC B5 CM CS D8D9D6D2B4CSD7 BC BN CSD6 BC B5 AX D8D9D6D2 CTD5B4CSD7BN CSD6B5BN D8D9D6D2 CTD5B4CSD7BN CSD7 BC B5 CM D8D9D6D2 CTD5B4CSD7 BC BN CSD7 BCBC B5 AX D8D9D6D2 CTD5B4CSD7BN CSD7 BCBC B5 CV CPD0D3D2CVB4CSD7BN D4CPBN CSCXD6B5 AX D8D4CPD8CWB4D4CPB5BN (20) CPD8B4CSD7BN D4B5 CM CPD8B4CSD7 BC BN D5B5 CM DI D8D6CPDACTD0B4CSD7BN CSD7 BC B5 AX (21) BLD4CPBN CSCXD6 A8 B4D4CPBN CSCXD6BN D4BN D5B5 CM CPD0D3D2CVB4CSD7BN D4CPBN CSCXD6B5 CM CPD0D3D2CVB4CSD7 BC BN D4CPBN CSCXD6B5 A9 BN CPD0D3D2CVB4CSD7BN D4CPBN CSCXD6B5 CM CPD0D3D2CVB4CSD7BN D4CPBDBN CSCXD6BDB5 AX D4CP BP D4CPBDBN (22) CPD8B4CSD7BN D4B5 CM CPD8B4CSD7 BC BN D4B5 CM CPD0D3D2CVB4CSD7BN D4CPBN CSCXD6B5 CM (23) CPD0D3D2CVB4CSD7 BC BN D4CPBN CSCXD6B5 AX D8CTD5B4CSD7BN CSD7 BC B5BN A8 CWCSD7BN D8D9D6D2 CSCTD7CRBN CSD7 BC CX CM D8D9D6D2 CSCTD7CR BIBP D8D9D6D2BTD6D3D9D2CS CM (24) CPD0D3D2CVB4CSD7BN D4CPBN CSCXD6B5 CM CPD0D3D2CVB4CSD7 BC BN D4CPBDBN CSCXD6BDB5 A9 AX D4CP BIBP D4CPBDBN CWCSD7BN D8D9D6D2BTD6D3D9D2CSBN CSD7 BC CX AX CPD0D3D2CVB4CSD7BN D4CPBN CSCXD6B5 AH CPD0D3D2CVB4CSD7 BC BN D4CPBN A0CSCXD6B5BN (25) B4D4CPBN D4D3D7BN D4BN D5B5 AH B4D4CPBN D2CTCVBN D5BN D4B5BN (26) BMB4D4CPBN CSCXD6BN D4BN D4B5BN (27) B4D4CPBN CSCXD6BN D4BN D5B5 CM B4D4CPBN CSCXD6BN D5BN D6B5 AX B4D4CPBN CSCXD6BN D4BN D6B5BN (28) B4D4CPBN CSCXD6BN D4BN D5B5 AX D2 CPD8CWB4D4CPBN D4B5 (29) D2 CPD8CWB4D4CPBN D4B5 CM D2 CPD8CWB4D4CPBN D5B5 CM D8D4CPD8CWB4D4CPB5 AX (30) BLCSD7BN CSD7 BC CUCPD8B4CSD7BN D4B5 CM CPD8B4CSD7 BC BN D5B5 CM D8D6CPDACTD0 CTD5B4CSD7BN CSD7 BC B5CVBN CUD1CXD2 D8D6CPDACTD0 CTD5 BM (31) D8CTD5B4CSD7BN CSD7 BC B5 CM D8CTD5B4CSD6BN CSD6 BC B5 CM CS D8D6CPDACTD0B4CSD7 BC BN CSD6 BC B5 AX D8D6CPDACTD0 CTD5B4CSD7BN CSD6B5BN D8D6CPDACTD0 CTD5B4CSD7BN CSD7 BC B5 CM D8D6CPDACTD0 CTD5B4CSD7 BC BN CSD7 BCBC B5 AX D8D6CPDACTD0 CTD5B4CSD7BN CSD7 BCBC B5 CV circ D8D4CPD8CW AV CPD0D3D2CV AV  AV D2CPD8CW AV D8D4D0CPCRCT var DI CBCBD4D6CTCS CV

Predicate D8CTD5 is the equivalence relation defined by axiom 14. D8CTD5B4CSD7BN CSD7 BC B5 is the case whenever CSD7 and CSD7 BC cannot be distinguished by views and actions (i.e. CRCTD5B4CSD7BN CSD7 BC B5) and it is consistent to group CSD7 and CSD7 BC into the same place. If we assume that views uniquely identify distinctive states (e.g. CE CXCTDBB4CSD7BN CE B5 CM CE CXCTDBB4CSD7 BC BN CE B5 AX CSD7 BP CSD7 BC ), then predicates CRCTD5 and D8CTD5 will reduce to equality. This is expected since all that is required to identify a distinctive state is its view.

Every distinctive state is at a unique place (Axiom 16). Whenever the agent D8D9D6D2D7, it stays at the same place (Axiom 17). Distinctive states grouped into a topological place should be D8D9D6D2 connected (modulo D8CTD5) (Axiom 18). Travel actions among distinctive states are abstracted to topological paths connecting the places associated with those distinctive states (Axiom 21). A distinctive state is along at most one path (Axiom 22). At each place there is at most one distinctive state along a given path direction (Axiom 23). Turn actions other than turnAround change the path the initial and final distinctive states are at (Axiom 24). TurnAround actions relate distinctive states being in the same path but opposite directions (Axiom 25). The order of places in a given path direction is the inverse of the order of places in the other path direction (Axiom 26). Axioms 27 and 28 require B4D4CPBN CSCXD6BN A1 BN A1B5 to be a non-reflexive transitive order for the places on D4CP. Places ordered by a path should belong to that path (Axiom 29). Axiom 30 requires the agent to have traveled among the places on a same path.

Our theory does not assume a "rectilinear" environment where paths intersect at most in one place. It is possible for different paths to have the same order of places (see Figure 4). Topological information can distinguish distinctive states not distinguishable by view and actions.

Example 3

Consider the scenario of example 1. Since the same view is experienced at a, b and c, the extent of CRCTD5 is maximized by declaring CRCTD5 BP D8D6D9CT. Using the topological theory, from axiom 16 we conclude that there exist places  and , such that CPD8B4CPBN B5 and CPD8B4CRBN B5. Since it is the case that DI D8D6CPDACTD0B4CPBN CRB5, from axioms 21 and 27 we conclude, for instance, that  BIBP . Distinctive states CP and CR are topologically distinguishable though they are "causally indistinguishable" (i.e. CRCTD5B4CPBN CRB5 CM BMD8CTD5B4CPBN CRB5). CUend of exampleCV

Given a minimal model  of CC CC B4BXB5, the SSH topological map is defined by the extent in of tpath, tplace, along, PO and at. Since the positive and negative direction of a path are chosen arbitrarily (Axiom 21), there is not a unique minimal model for CCCCB4BXB5. We will consider these "up to path direction isomorphic" models to be the same. However, it is still the case that the theory CCCCB4BXB5 has minimal models that are not isomorphic up to path direction (see Figure 5).

5 SSH Boundary Regions

In addition to connectivity and order among places and paths, the topological map includes topological boundary relations: assertions that a place lies to the right of, to the left of, or on a path. In order to determine boundary relations we formally state the following default heuristic. Suppose the agent is at an intersection on a given path, and it then turns right. If the agent now travels, any place it finds while traveling with no turns will be on the right of the starting path. When conflicting information exists about whether a place is to the right or left of a path, we deduce no boundary relation (see Figure 6).

We use the predicates CC D3D8CWCTCACXCVCWD8CU BPCC D3D8CWCTCTCU D8CU B4D4BDBN D4CPBN CSCXD6BN D4CPBDBN CSCXD6BDB5 to represent the facts that (i) p1 is a place on both paths, pa and pa1, and (ii) when the agent is at place p1 facing in the direction dir of pa, after executing a turn right (left) action, the agent will be facing on the direction dir1 of pa1 (see Figure 7). The predicates TotheLeftOf and TotheRightOf are derived from the actions performed by the agent at a place:

We use the predicates CTCUD8CUB4D4CPBN CSCXD6BN D0D6B5 and CACXCVCWD8CUB4D4CPBN CSCXD6BN D6D6B5 to denote that region D0D6 (D6D6) is the left (right) region of path pa with respect to the path's direction dir. The left/right regions of a path are unique, disjoint, and related when changing the path direction (i.e CTCUD8CUB4D4CPBN CSCXD6BN D6B5 AH CACXCVCWD8CUB4D4CPBN A0CSCXD6BN D6B5). From the relative orientation between paths at a place, we deduce the relative location of places with respect to a path (see Figure 7): 12

The predicate Ab is the standard "abnormality" predicate used to represent defaults in circumscriptive theories [Lifschitz, 1994]. Axiom 33 states that "normally", if at place p1 path pa1 is to the right of path pa, and place p is after p1 on path pa1, then it should be the case that p is on the right of pa (Figure 7). In order to capture this default, boundary regions domain theory axioms 13 are added to the block AT block (see Figure 3). Since we are interested in the extent of the new predicates in region, LeftOf, RightOf, TotheLeftOf and TotheRightOf, we allow them to vary in the circumscription policy. The new circumscription policy becomes

where DI D2CTDBCBCBD4D6CTCS stands for the tuple of predicates at, along, teq , travel eq, turn eq, LeftOf, RightOf, TotheLeftOf, and TotheRightOf. The circumscription policy states that boundary relations should be established even at the expense of having more places on the map. In addition, by minimizing the predicates is region and in region, we require the models of our theory to have only the regions that are explicitly created by the agent, and not arbitrary ones.

Example 4

Boundary relations determine distinctions among environment states that could not be derived from the connectivity of places alone. Consider an agent visiting the different corners of a square room in the order suggested by Figure 8a. In addition, suppose the agent defines views by characterizing the direction of walls and open space. Accordingly, the agent experiences four different views, v1-v4, in this environment.

The set of experiences E in the environment are:

CE CXCTDBB4CSD7BDBN DABDB5 CE CXCTDBB4CSD7BEBN DABEB5 CE CXCTDBB4CSD7BFBN DABDB5 CE CXCTDBB4CSD7BGBN DABEB5 CE CXCTDBB4CSD7BHBN DABDB5 CWCSD7BDBN D8D9D6D2CACXCVCWD8BN CSD7BECX CWCSD7BEBN D8D6CPDACTD0BN CSD7BFCX CWCSD7BGBN D8D6CPDACTD0BN CSD7BHCX CWCSD7BFBN D8D9D6D2CACXCVCWD8BN CSD7BGCX

Suppose that the agent does not use boundary regions when building the topological map. Then the minimal topological model associated with E has two paths 14 and two places. In this model, D8CTD5B4CSD7BDBN CSD7BHB5 is the case. The environment looks perfectly symmetric to the agent (Figure 8b).!!

Suppose now that the agent relies on boundary regions. Let P, Q, R, be the topological places associated with ds1, ds3 and ds5 respectively. From Axiom 21, let Pa, Pb, CSCXD6 CP and CSCXD6 CQ be such that B4CPBN CSCXD6 CP BN BN B5, CPD0D3D2CVB4CSD7BEBN  CPBN CSCXD6 CP B5, CPD0D3D2CVB4CSD7BFBN  CPBN CSCXD6 CP B5, B4CQBN CSCXD6 CQ BN BNCAB5, CPD0D3D2CVB4CSD7BGBN  CQBN CSCXD6 CQ B5, and CPD0D3D2CVB4CSD7BHBN CQBN CSCXD6 CQ B5 hold. From Axiom 32 we can conclude then CCD3D8CWCTCACXCVCWD8CUB4 BN CPBN CSCXD6 CP BN CQBN CSCXD6 CQ B5. In the proposed model, the extent of Ab is minimized by declaring BTCQ BP CUCPD0D7CT and consequently from Axiom 33 we conclude CXD2 D6CTCVCXD3D2B4CABN D6CXCVCWD8B4CPBN CSCXD6 CP B5B5 where D6CXCVCWD8B4CPBN CSCXD6 CP B5 denotes the right region of CP when facing CSCXD6 CP . Finally, since a path and its regions are disjoint, and D2CPD8CWB4CPBN B5 is the case, we conclude  BIBP CA and so BIBP D8CTD5B4CSD7BDBN CSD7BHB5. The resulting topological map is depicted in Figure 8c. CUend of exampleCV

12 The predicate in region(p,r) states that place p is in region r.

13 In the spirit of axioms 32-33.

14 Notice that from CWCSD7BFBN D8D9D6D2CACXCVCWD8BN CSD7BGCX and Axiom 24 we can deduce that CP BIBP CQ in Figure 8b.

If the agent's sensory capabilities are so impoverished that many distinctive states are perceived to be similar, then metrical information could be used to distinguish different environment states. Figure 9 summarizes different representations an agent could build depending on the spatial properties it relies on.

6 Conclusions

Starting with an informal description of the SSH we have formally specified its intended models. These models correspond to the models of the circumscriptive theory TT(E). The formal account of the theory allows us to illustrate the deductive power of the different SSH ontologies. For instance, example 4 shows how the use of boundary relations allows the agent to determine distinctions among environment states that could not be derived from the connectivity of places and paths alone.

The theory TT(E) is rather complex so it may be difficult to determine the effect of the different defaults in combination. However, it is possible to translate this theory into a logic program whose answer sets determine the models of TT(E). We have illustrated the case for the SSH causal theory CT(E), but the same techniques apply for TT(E). The major subtleties in the translation are the minimality and maximality conditions associated with the theory. We have used Smodels to calculate the models of TT(E) and confirm that the theory yields the intended models. However, when the number of distinctive states is big, Smodels may not be able to ground the theory as the number of rules associated with the program grows exponentially. We are still working on solving this problem.

Acknowledgments

We are grateful to Vladimir Lifschitz for his valuable feedback during this work and for suggesting the use of Smodels to implement the ideas proposed here. We also thank the anonymous referees for their valuable comments on this paper.