Abstraction of Agents Executing Online and their Abilities in the Situation Calculus

1 Introduction

One way to effectively support reasoning about agents with complex behavior is to use abstraction. In essence, this involves developing an abstract model of the agent/domain that suppresses less important details. The abstract model allows us to reason more easily about the agent's possible behaviors and to provide high-level explanations of the agent's behavior. In AI, abstraction has been investigated in variety of settings such as to improve efficiency in planning (e.g., [Baier and McIlraith, 2006; Kuter et al., 2007]), facilitate verification (e.g., [Mo et al., 2016]), and capture the social practices of multi-agent systems (e.g., [Dignum et al., 2015]).

[Banihashemi et al., 2017] proposed a general framework for agent abstraction based on the situation calculus [McCarthy and Hayes, 1969; Reiter, 2001] and the ConGolog agent programming language [De Giacomo et al., 2000]. They assume that one has a high-level/abstract action theory, a low-level/concrete action theory, both representing the agent's behavior at different levels of detail, and a refinement mapping between the two. The mapping associates each high-level primitive action to a ConGolog program defined over the low-level action theory that "implements it". Moreover, it maps each high-level fluent to a state formula in the low-level language that characterizes the concrete conditions under which it holds. They then define a notion of a high-level theory being a sound abstraction of a low-level theory under a given refinement mapping. The formalization involves the existence of a suitable bisimulation relation [Milner, 1971;

1989] between models of the low-level and high-level theories. It is shown that sound abstractions have many useful properties that ensure that one can reason about the agent's actions (e.g. executability, projection, and planning) at the abstract level, and refine and concretely execute them at the low level.

In this paper, we study how we can apply this framework in the case where the agent is executing online [De Giacomo and Levesque, 1999; Sardi˜na et al., 2004b], i.e., may acquire new knowledge while executing (e.g., by sensing). This means that the knowledge base that the agent uses in her reasoning needs to be updated during the execution.

To formalize a notion of sound abstraction in online executions, we first identify a sufficient property for sound abstraction to persist in online executions. We then show that a key result about sound abstractions extends to online executions. We also adapt definitions of strategies and ability to perform a task/achieve a goal [Moore, 1985; Lesp´erance et al., 2000; 2008] to our model of online execution. Then, we show our main result, namely that under some reasonable assumptions, if we have a sound abstraction and the agent has a strategy by which she is able to achieve a goal at the high level, then one can refine it into a low-level strategy by which the agent is able to achieve the refinement of the goal. Moreover, the low-level strategy can be obtained piecewise/incrementally, by finding a refinement of each step of the high-level strategy individually. This makes reasoning about agents' abilities much easier.

Let us briefly discuss related work. [Giunchiglia and Walsh, 1992; Nayak and Levy, 1995] formalize abstraction of static logical theories; instead, our work focuses on abstraction of dynamic domains where the agent may acquire new information as it executes. Other related work focuses on planning, for instance [Gabaldon, 2002], which studies encodings of HTNs in ConGolog with enhanced features like exogenous actions and online executions, and [Baier and McIlraith, 2006], which investigates planning with sensing and complex/macro actions specified in Golog. The former uses a single basic action theory (BAT), while the latter compiles the abstracted actions into a new BAT that includes both the original and abstracted actions. Our approach is more general and allows fluents to be abstracted as well.

In the next section, we outline the basics of the Situation Calculus and ConGolog. Then in Section 3, we review the agent abstraction framework of [Banihashemi et al., 2017]. Following that in Section 4, we discuss how we model sensing, exogenous actions, and online execution. Then in Section 5, we identify sufficient conditions for sound abstractions to persist in online executions and examine their properties. Following that in Section 6, we formalize a suitable notion of agent ability. Then in Section 7, we present our main result, i.e., that under a reasonable set of assumptions, when an agent has a strategy by which she is able to achieve a goal at the high level, we can refine it into a low-level strategy to do so. The paper then concludes by discussing our contributions and topics for future work.

2 Preliminaries

Situation Calculus. The situation calculus is a well known predicate logic language for representing and reasoning about dynamically changing worlds. Within the language, one can formulate basic action theories (BATs) that describe how the world changes as a result of actions; see [Reiter, 2001] for details of how these are defined. Hereafter, we will use D to refer to the BAT under consideration. We assume that there is a finite number of action types A. Moreover, we assume that the terms of object sort are in fact a countably infinite set N of standard names for which we have the unique name assumption and domain closure. For simplicity, and w.l.o.g., we assume that there are no functions other than constants and no non-fluent predicates. We write do([a1, a2, . . . , an-1, an], s) as an abbreviation for the situation term do(an, do(an-1, . . . , do(a2, do(a1, s)) . . .)); for an action sequence ⃗a, we often write do(⃗a, s) for do([⃗a], s). A special predicate Poss(a, s) is used to state that action a is executable in situation s. The abbreviation Executable(s) means that every action performed in reaching situation s was executable in the situation in which it occurred.

ConGolog. To represent and reason about complex actions or processes obtained by suitably executing atomic actions, various so-called high-level programming languages have been defined [Levesque et al., 1997]. Here we concentrate on (a variant of) ConGolog [De Giacomo et al., 2000] that includes the following constructs:

In the above, nil denotes the empty program, which does nothing and is already terminated, α is an action term, possibly with parameters, and ϕ is situation-suppressed formula, i.e., a formula with all situation arguments in fluents suppressed. As usual, we denote by ϕ[s] the formula obtained from ϕ by restoring the situation argument s into all fluents in ϕ. The sequence of program δ1 followed by program δ2 is denoted by δ1; δ2. Program δ1|δ2 allows for the nondeterministic choice between programs δ1 and δ2, while πx.δ executes program δ for some nondeterministic choice of a legal binding for object variable x (observe that such a choice is, in general, unbounded). δ∗ performs δ zero or more times. Program δ1‖δ2 expresses the concurrent execution (interpreted as interleaving) of programs δ1 and δ2.

Formally, the semantics of ConGolog is specified in terms of single-step transitions, using the following two predicates: (i) Trans(δ, s, δ′ , s′ ), which holds if one step of program δ in situation s may lead to situation s′ with δ′ remaining to be executed; and (ii) Final(δ, s), which holds if program δ may legally terminate in situation s. The definitions of T rans and Final we use are as in [De Giacomo et al., 2010]; differently from [De Giacomo et al., 2000], the test construct ϕ? does not yield any transition, but is Final when satisfied. Predicate Do(δ, s, s′ ) means that program δ, when executed starting in situation s, has s′ as a legal terminating situation, and is defined as Do(δ, s, s′ ) .= ∃δ′ .Trans∗ (δ, s, δ′ , s′ ) ∧ Final(δ′ , s′ ) where Trans∗ denotes the reflexive transitive closure of Trans. In the rest, we use C to denote the axioms defining the ConGolog programming language.

Situation-Determined Programs. A ConGolog program δ is situation-determined (SD) in a situation s [De Giacomo et al., 2012] if for every sequence of actions, the remaining program is determined by the resulting situation, i.e.,

For instance, the program a; (b | c) (assuming the actions involved are always executable) is SD in situation S0, since there is a unique remaining program (b | c) in do(a, S0) (and similarly for the other reachable situations). However, the program (a; b) | (a; c) is not SD in situation S0, since after performing action a, and given only the situation do(a, S0), it is impossible to determine what the remaining program is (it could be either b or c).

3 Abstracting Agent Behavior

In the agent abstraction framework of [Banihashemi et al., 2017], there is a high-level (HL) action theory Dh and a lowlevel (LL) action theory Dl representing the agent's possible behaviors at different levels of detail. Dh (resp. Dl ) involves a finite set of primitive action types Ah (resp. Al ) and a finite set of primitive fluent predicates Fh (resp. Fl ). Also, Dh and Dl are assumed to share no domain specific symbols except for the set of standard names for objects N.

Refinement Mapping. To relate the two theories, a refinement mapping m is defined as a function that associates each high-level primitive action type A in Ah to a situationdetermined ConGolog program δA defined over the low-level theory that implements the action, i.e., m(A(⃗x)) = δA(⃗x); moreover, m maps each situation-suppressed high-level fluent F(⃗x) in Fh to a situation-suppressed formula φF (⃗x) defined over the low-level theory that characterizes the concrete conditions under which F(⃗x) holds in a situation. We extend the notation so that m(φ) stands for the result of substituting every fluent F(⃗x) in situation-suppressed formula φ by m(F(⃗x)). Also, we apply m to action sequences with m(α1, . . . , αn) .= m(α1); . . . ;m(αn) for n ≥ 1 and m(ϵ) .= nil, where ϵ is the empty sequence of actions.

m-Bisimulation. To relate the high-level and low-level models/theories, a variant of bisimulation [Milner, 1971; 1989] is defined as follows. Given Mh a model of Dh ∪ C, and Ml a model of Dl ∪ C, a relation B ⊆ ∆Mh S × ∆Ml S (where ∆MS stands for the situation domain of M) is an mbisimulation relation between Mh and Ml if 〈sh, sl〉 ∈ B implies that: (i) sh ∼Mh,Ml m sl, i.e., sh and sl evaluate each high-level primitive fluent the same; 1 (ii) for every high-level primitive action type A in Ah, if there exists s′h such that Mh |= Poss(A(⃗x), sh) ∧ s′h = do(A(⃗x), sh), then there exists s′l such that Ml |= Do(m(A(⃗x)), sl, s′l ), and 〈s′h , s′l 〉 ∈ B; and, (iii) for every high-level primitive action type A in Ah, if there exists s′l such that Ml |= Do(m(A(⃗x)), sl, s′l ), then there exists s′h such that Mh |= Poss(A(⃗x), sh) ∧ s′h = do(A(⃗x), sh) and 〈s′h , s′l 〉 ∈ B. Mh is m-bisimilar to Ml, written Mh ∼m Ml, if and only if there exists an m-bisimulation relation B between Mh and Ml such that (SMh 0 , SMl 0 ) ∈ B.

Sound Abstractions. In [Banihashemi et al., 2017], Dh is a sound abstraction of Dl relative to refinement mapping m if and only if, for all models Ml of Dl ∪ C, there exists a model Mh of Dh ∪ C such that Mh ∼m Ml. With a sound abstraction, whenever the high-level theory entails that a sequence of actions is executable and achieves a certain condition, then the low level must also entail that there exists an executable refinement of the sequence such that the "translated" condition holds afterwards. Moreover, whenever the low level considers the executability of a refinement of a high-level action to be satisfiable, then the high level does also. Sound abstractions can be used to perform effectively several forms of reasoning about action, such as planning, monitoring, and generating high-level explanations of low-level behavior. Note that a dual notion is also defined: Dh is a complete abstraction of Dl relative to refinement mapping m if and only if, for all models Mh of Dh ∪C, there exists a model Ml of Dl ∪C such that Ml ∼m Mh.

Example 1 For our running example, we consider a travel planner agent that can book a seat (economy Ec or business Bz) on a flight f for a customer c. The high-level BAT Deg h abstracts over details of the booking procedure. The fluent Upg(c, s) holds when an upgrade for customer c is possible. The action book(c, cls, f) (where cls denotes either Bz or Ec) is always possible for economy seats but only possible for business seats when Upg(c, s) holds. The fluent Booked(c, cls, f, s) indicates a ticket has been booked for c. The low-level BAT Deg l models the process of booking a ticket in more detail. Two types of upgrades exist: AirMiles(c, s) and Promotion(c, s). Action selFlt(c, cls, f) to select a flight is only possible for Bz seats if either of AirMiles(c, s) or Promotion(c, s)

1 This defines a local condition for the bisimulation. We say that situation sh in Mh is m-isomorphic to situation sl in Ml, written sh ∼Mh,Ml m sl, if and only if Mh, v[s/sh] |= F(⃗x, s) iff Ml, v[s/sl] |= m(F(⃗x))[s] for every high-level primitive fluent F(⃗x) in Fh and every variable assignment v (v[x/e] stands for the assignment that is like v except that x is mapped to e).

holds and action pay(c, cls, f) makes payments. Fluents Selected(c, cls, f, s) and Paid(c, cls, f, s) indicate the ticket has been selected and paid for respectively. The refinement mapping meg is defined as:

meg (Upg(c)) = AirMiles(c) ∨ P romotion(c) meg (Booked(c, cls, f )) = Selected(c, cls, f ) ∧ P aid(c, cls, f ) meg (book(c, cls, f )) = selF lt(c, cls, f ); pay(c, cls, f )

4 Online Execution and Sensing

In this paper, similarly to [Lesp´erance et al., 2008], we model sensing as an ordinary action which queries a sensor, followed by the reporting of a sensor result, in the form of an exogenous action. With this way of doing sensing, we essentially store the sensing results in the situation (which includes all actions executed so far including the exogenous actions used for sensing). We update the theory/knowledge base (KB) to incorporate the sensed information by asserting Poss(a, s) atoms and relying on precondition axioms to relate sensing to fluents. In particular the current KB after having performed the sequence of actions ⃗a is D ∪ C ∪ {Executable(do(⃗a, S0)}, which we abbreviate as D ∪ C ∪ Sensed(⃗a). Note that this also handles the agent's acquiring knowledge from an arbitrary exogenous action.

Example 2 To allow the high-level agent in Example 1 to learn if Upg(c, s) holds, Deg h can include the following:

where qryUpg(c) is an ordinary action that is used to query (i.e., sense) if Upg(c, s) holds and repUpg(c, x) is an exogenous action that informs the agent if Upg(c, s) holds through its precondition axiom; repUpg(c, 1) is executed if Upg(c, s) holds, and otherwise, repUpg(c, 0) is executed. The fluent QrdUpg(c, s) (resp. RecvRep(c, s)) in the precondition indicates whether action qryUpg(c) (resp. repUpg(c, x)) has already been performed in s. (The low-level BAT can be extended in a similar way to support sensing whether upgrades are possible through air miles and promotions.)

We model an online agent configuration (c) as a pair 〈δ, ⃗a〉, where δ is the remaining program and ⃗a is the sequence of actions performed so far starting from S0. The initial configuration ci is 〈δi , ϵ〉. [Banihashemi et al., 2016], define the online transition relation between configurations as follows:

〈δ,⃗a〉 →A(⃗n) 〈δ′ ,⃗aA(⃗n)〉 if and only if either A ∈ Ao , ⃗n ∈ N k and D ∪ C ∪ Sensed(⃗a) |= T rans(δ, do(⃗a, S0), δ′ , do(A(⃗n), do(⃗a, S0))) or A ∈ Ae , ⃗n ∈ N k and D∪ C ∪ Sensed(⃗a) ∪ {T rans(δ, do(⃗a, S0), δ′ , do(A(⃗n), do(⃗a, S0)))} is satisfiable,

where Ao (resp. Ae ) represents the ordinary (resp. exogenous) set of action types. Here, 〈δ,⃗a〉 →A(⃗n) 〈δ′ ,⃗aA(⃗n)〉 means that configuration 〈δ,⃗a〉 can make a single-step online transition to configuration 〈δ′ ,⃗aA(⃗n)〉 by performing action A(⃗n). If A(⃗n) is an ordinary action, the agent must know that the action is executable and know what the remaining program is afterwards. If A(⃗n) is an exogenous action, the agent need only think that the action may be possible with δ′ being the remaining program. The relation c →∗ ⃗a c′ is the reflexive-transitive closure of c →A(⃗n) c′ denoting that online configuration c′ can be reached from configuration c by performing a sequence of online transitions involving the sequence of actions ⃗a. A (meta-theoretic) predicate c✓, meaning that configuration c is known to be final, is defined as:

〈δ, ⃗a〉✓ if and only if D ∪ C ∪ Sensed(⃗a) |= F inal(δ, do(⃗a, S0)).

5 Sound Abstraction in Online Executions

How can we use abstraction in agents that execute online and acquire new information during a run? The agent's theory/KB is updated when it gets new information. The first question is whether a sound abstraction remains so when that happens.

Example 3 Suppose that we have a high-level exogenous action ah that is executable if and only if Ph holds. Let m(Ph) = Pl and m(ah) = Pl?; al, where al is a low-level exogenous action. Moreover, assume that at the low level, al is always executable. Initially, it is unknown whether Ph holds at the high level and similarly for Pl at the low level. It is easy to check that Dh is a sound abstraction of Dl with respect to the mapping m. However, if ah and its refinement al occur and the theories are updated, then Dh∪{Poss(ah, S0)} is no longer a sound abstraction of Dl ∪ {Poss(al, S0)} wrt m. In do(ah, S0), the high-level agent has learned that Ph holds, as Poss(ah, S0) has been added to the theory. However, at the low level, adding Poss(al, S0) has no effect and in do(al, S0), it is still unknown whether Pl holds. The updated low-level theory has a model where ¬Pl holds, which has no m-bisimilar model in the updated high-level theory.

Thus a sound abstraction does not always remain so when we update the theories after an action is executed online. For the sound abstraction to persist, we need to ensure that the low level acquires as much information as the high level, e.g., ensure that the low level learns that m(Ph), i.e., Pl, holds. When a high-level action a occurs, the high level learns that a was executable. If the low level also learns that it has in fact just executed a refinement of a, then we can be certain that it has acquired as much information as the high level. We can generalize this to action sequences and prove that it is a sufficient condition for the sound abstraction to persist: 2

Theorem 1 (Online Persistence of Sound Abstractions) If Dh is a sound abstraction of Dl relative to mapping m and Dl ∪ C ∪ Sensed(⃗a) |= Do(m(⃗α), S0, do(⃗a, S0)), then Dh ∪ Sensed(⃗α) is a sound abstraction of Dl ∪ Sensed(⃗a) wrt m.

Here, the condition Dl ∪ C ∪ Sensed(⃗a) |= Do(m(⃗α), S0, do(⃗a, S0)) ensures that after executing a refinement ⃗a of highlevel action sequence ⃗α, the low level knows it has just executed a refinement of ⃗α, and thus it has learned as much as the high level did, and we still have a sound abstraction. 3

2 For proofs of our results, see [Banihashemi et al., 2018a].

We can use the above to extend the results of [Banihashemi et al., 2017] on sound abstractions so that the agent gets to use the knowledge acquired in an online execution. We can show that if after executing action sequence ⃗α online the high level knows that it can execute action sequence ⃗ β to achieve condition φ, then after executing a refinement ⃗a of ⃗α online, being aware that ⃗a is a refinement of ⃗α, the low level also knows that there exists a refinement of ⃗ β that achieves m(φ):

Proposition 2 Suppose that Dh is a sound abstraction of Dl relative to mapping m and Dl ∪ C ∪ Sensed(⃗a) |= Do(m(⃗α), S0, do(⃗a, S0)) for some ground high-level action sequence ⃗α and ground low-level action sequence ⃗a. Then for any high-level ground action sequence ⃗ β and situationsuppressed formula φ,

if Dh∪Sensed(⃗α) |= Executable(do(⃗α⃗ β, S0)) ∧ φ[do(⃗α⃗ β, S0)], then Dl∪C∪Sensed(⃗a) |= ∃s.Do(m(⃗ β), do(⃗a, S0), s) ∧ m(φ)[s].

Now, if we had complete information and a deterministic environment, then we could use this proposition to extract a plan at the low level to realize high-level action sequence ⃗ β and achieve φ. However neither of these two conditions hold in the case we are studying. The agent has incomplete information and uses sensing to acquire the knowledge she needs. Moreover the environment is nondeterministic and produces exogenous actions that are not under the control of the agent. For these reasons, we cannot make use of this proposition. Instead, for the agent to be able to achieve a goal, she needs to have a strategy that ensures achieving the goal no matter how the environment behaves and how sensing turns out. To address this, we next develop an account of agent ability. Subsequently, we return to how abstraction can be exploited to find strategies and ensure ability.

6 Agent Ability

Intuitively, an agent is able to perform a task/achieve a goal if she can always choose an action that eventually leads to successful completion of the task/achievement of the goal no matter how the environment behaves and what information she finds out; i.e., she needs to have a strategy that she can follow to successfully complete the task/achieve the goal, where the strategy specifies how she should continue to act after the environment performs some action in response to what has occurred so far. Note that we assume that environment actions are fully observable. Ability is similar to the concept of conditional or contingent planning [Cimatti et al., 2003; Alford et al., 2009; Geffner and Bonet, 2013], where agents operating online in dynamic and incompletely known environments need to construct plans/strategies that prescribe different behaviors depending on new information acquired

3 This condition does not seem too difficult to guarantee in practice. Essentially, we must ensure that whenever a test succeeds in a refinement of a high-level action, the low level knows or learns the test was satisfied. E.g., we can redefine m(ah) = Pl?; confirmPl ; al, where confirmPl is a new exogenous action that has Pl as precondition and no effects; this ensures that when m(ah) is executed, the agent learns that m(Ph), i.e., Pl, holds.

(e.g., as a result of sensing) to ensure they achieve their goals/execute their tasks.

TurnTaking. To formalize ability, we need to specifywhen the agent/environment can act. We do this by enforcing turn taking between the agent and the environment. We assume that in any situation, either it is the agent's turn and all the executable actions are ordinary, or it is the environment's turn and all the executable actions are exogenous: 4

Assumption 1 (Turn Taking) For D ∈ {Dh, Dl}, we have

Furthermore, we assume that in any online configuration, 5 it is known whether it is the agent's or the environment's turn:

Assumption 2 (Always Known Whose Turn It Is) For D ∈ {Dh,Dl} and for all ground sequences ⃗a such that 〈(πa.a)∗ , ϵ〉 →∗ ⃗a 〈δ,⃗a〉 and 〈δ,⃗a〉✓ for some δ, we have that

Able By. Here, we will restrict attention to bounded-length strategies. 6 We represent (bounded) strategies γ as a restricted form of program using the following syntax:

i ; γi].

Here, αo ranges over ordinary action terms, βe i over exogenous action terms, and γi over strategies, and set(·) is an infinitary version of nondeterministic branch [De Giacomo et al., 2012]. Thus nil is the strategy that does nothing and stops, [αo ; γ] represents the strategy where the agent does action αo and then follows strategy γ, and set([βe 1 ; γ1], [βe 2 ; γ2], . . .) with distinct actions βe 1 , βe 2 , . . . represents the strategy where exogenous action βe 1 may occur after which γ1 is followed, exogenous action βe 2 may occur after which γ2 is followed, etc.; there may be a finite or countably infinite set of such pairs [βe i ; γi].

We adapt [Lesp´erance et al., 2008] and define AbleBy(δ,⃗a, γ), meaning that the agent is able to successfully perform a task represented by an online situationdetermined program 7 δ in an environment that behaves as specified by δ in situation do(⃗a, S0) by executing the strategy γ, to be the smallest relation R(δ,⃗a, γ) such that:

4 If at some point, the "player" whose turn it is has the option of doing nothing, we can have it execute a "no-op" action.

5 Note that (πa.a)∗ is a program that repeatedly executes a nondeterministically chosen primitive action zero or more times; thus it can perform any sequence of executable actions.

6 For more general types of tasks that require unbounded strategies, one can use an approach like [Sardi˜na et al., 2004a; 2006].

7 A program is online situation-determined if for any sequence of actions that the agent can perform online, the resulting agent configuration is unique [Banihashemi et al., 2016].

• (A) for all pairs (δ,⃗a), if 〈δ,⃗a〉✓, then R(δ,⃗a, nil);
• (B) for all δ,⃗a, if there exists a, δ′ such that a ∈ Ao and 〈δ,⃗a〉 →a 〈δ′ ,⃗aa〉 and R(δ′ ,⃗aa, γ), then R(δ,⃗a, [a; γ]);
• (C) for all δ,⃗a, if there exists a, δ′ such that a ∈ Ae and 〈δ,⃗a〉 →a 〈δ′ ,⃗aa〉 and for all a, δ′ such that 〈δ,⃗a〉 →a 〈δ′ ,⃗aa〉 there exists γ such that R(δ′ ,⃗aa, γ), then R(δ, ⃗a, set(E)) where E =

That is, (A) if δ is final in situation do(⃗a, S0), then the agent is able to execute δ in situation do(⃗a, S0) by performing the empty strategy (nil); (B) if there is an ordinary action a that the agent can execute online to get from the current configuration 〈δ,⃗a〉 to some configuration 〈δ′ ,⃗aa〉 after which the agent is able to execute δ′ in situation do(⃗aa, S0) by following strategy γ, then the agent is able to execute δ in situation do(⃗a, S0) by following strategy [a; γ]; (C) if there is some exogenous action a that can be executed online from 〈δ,⃗a〉 and for every exogenous action a that can be executed online from the current configuration 〈δ,⃗a〉 to some configuration 〈δ′ ,⃗aa〉 there exists a strategy γ such that the agent is then able to execute δ′ in situation do(⃗aa, S0) by following strategy γ, then the agent is able to execute δ in situation do(⃗a, S0) by following strategy set(E), where E is the set of all such pairs [a; γ]. Note that the task of simply achieving a goal φ (by performing some arbitrary action sequence) can be represented by the programAchieve(φ) .= (πa.a)∗ ; φ?.

Example 4 Returning to our running example, consider the task δh1 = Achieve(φh1), where φh1 = (Upg(C1) ∧ Booked(C1,Bz, F1)) ∨ (¬Upg(C1) ∧ Booked(C1,Ec, F1)), i.e., book a business seat for customer C1 on flight F1 if an upgrade is available and otherwise book an economy seat. Then at the high level, we have AbleBy(δh1 , ϵ, γh1 ) with the strategy γh1 = qryUpg(C1); set((repUpg(C1, 1); book(C1, Bz, F 1); nil), (repUpg(C1, 0); book(C1, Eco, F 1); nil)).

7 Hierarchical Refinement of Abilities

The notions of ability and strategy we have defined can be used at both the high and low levels. If we have a strategy at the high level that the agent can follow to perform a task or achieve a goal, under what conditions can we obtain a strategy at the low level that refines this high-level strategy and that the agent can follow to perform a refinement of the high-level task or achieve a refinement of the high-level goal? What assumptions are sufficient to ensure we can always do this?

High-Level Monitorability. We assume the agent only executes low-level action sequences that refine some high-level action sequence, i.e., the agent is high-level monitorable.

Assumption 3 (All LL behaviors refine HL actions)

Dl ∪ C |= ∀s.Executable(s) ⊃ ∃δ.T rans∗ (ANYSEQHL, S0, δ, s) where ANYSEQHL .= (|Ai∈Ah π⃗x.m(Ai(⃗x)))∗ , i.e., do any sequence of refinements of high-level actions.

Without high-level monitorability, at the concrete level, there is nothing preventing the environment from performing an action that is not part of any refinement of a high-level action when it is its turn. Thus, if we have a strategy at the high level that achieves a goal/performs a task, it becomes irrelevant and it is impossible to realize this strategy at the low level; we can't use reasoning at the high level to guide the reasoning at the low level.

Low-Level Accountability. If it is the agent's turn at the high level and some ordinary action is executable online there, then as we have a sound abstraction, it follows that it is known that some refinement of it is executable at the low level. If instead it is the environment's turn and it is satisfiable that some exogenous action is executable at the high level, then sound abstraction is not sufficient to ensure that it is satisfiable that a refinement of a high-level exogenous action is executable at the low level. We need to avoid such cases, where an online transition exists at the high level, while the low level blocks, as no refinement of a high level action is executable. 8 Hence, we assume that after any sequence of refinements of high-level actions, i.e., in any situation s such that Do(ANYSEQHL, S0, s), if no refinement of any ordinary action is executable, then some refinement of some exogenous action is executable:

Assumption 4 (LL Exogenous Action Accountability)

where Aohl (resp. Aehl ) represents the high-level ordinary (resp. exogenous) set of action types.

We also need another assumption to ensure that the highlevel theory remains a sound abstraction of the low-level theory with respect to the mapping when a refinement of a highlevel action is executed and the agent may obtain new knowledge. Therefore, we assume that along all online executions, whenever a refinement of a high-level action has been executed, the low-level agent knows that it has executed it:

Assumption 5 (Awareness of Executed HL Actions) For all ground high-level action sequences ⃗α and all ground low-level action sequences ⃗a, if 〈m(⃗α), ϵ〉 →∗ ⃗a 〈δl,⃗a〉 and 〈δl,⃗a〉✓ for some δl, then Dl ∪ C ∪ Sensed(⃗a) |= Do(m(⃗α), S0, do(⃗a, S0)).

Together, these assumptions amount to low-level accountability: the low level accounts for high-level ordinary actions because we have a sound abstraction, it accounts for highlevel exogenous actions by Assumption 4, and it remains aware of the high-level actions executed by Assumption 5.

Local Refinement Enforceability. Assumptions 4 and 5 ensure that the low-level accounts for what happens at the high level, but does not guarantee its (local) enforceability, i.e., it does not guarantee the existence of strategies for the agent to enforce that refinements are successfully executed.

8 Instead, we could assume the high-level theory is both a sound and complete abstraction of the low-level theory with respect to a mapping. However, this seems more restrictive; moreover, it would require showing that completeness is preserved as we execute the high-level strategy. We will investigate this in future work.

With respect to ordinary actions, (local) refinement enforceability requires that if it is known that there exists a refinement of an ordinary high-level action β that is executable at the low level then the agent has a strategy to successfully execute a refinement of β, no matter what the environment does. We assume this holds in every online configuration:

Assumption 6 (Ability to Execute Ordinary HL Actions) For all ground high-level action sequences ⃗α and all ground low-level action sequences ⃗a such that 〈m(⃗α), ϵ〉 →∗ ⃗a 〈δl,⃗a〉 and 〈δl,⃗a〉✓ for some δl, and for any ground high-level ordinary action β ∈ Ao , if Dl ∪C ∪Sensed(⃗a) |= ∃s.Do(m(β), do(⃗a, S0), s), then there exists a low-level strategy γl such that AbleBy(m(β),⃗a, γl).

If Dh ∪ Sensed(⃗α) is a sound abstraction of Dl ∪ Sensed(⃗a) wrt mapping m and it is known at the high level that an ordinary action β is executable in do(⃗α, S0), it follows that a refinement of β is known to be executable at the low level in do(⃗a, S0), and thus by Assumption 6, there is a strategy to successfully execute a refinement of β at the low level.

With respect to exogenous actions instead, we want to ensure that if a refinement of a high-level exogenous action is possibly executable, then a refinement of some exogenous action will eventually be successfully executed online no matter how the agent and environment choose to act.

To formalize this, similar to [Lesp´erance, 2002], we define a predicate NecTerminates(δ,⃗a), meaning that all online executions of program δ in situation do(⃗a, S0) successfully terminate, as the least relation R(δ,⃗a) such that:

• (A) for all pairs (δ,⃗a), if 〈δ,⃗a〉✓and there does not exist a, δ′ such that 〈δ,⃗a〉 →a 〈δ′ ,⃗aa〉, then R(δ,⃗a);
• (B) for all pairs (δ,⃗a), if there exists a, δ′ such that 〈δ,⃗a〉 →a 〈δ′ ,⃗aa〉 and for all a, δ′ such that 〈δ,⃗a〉 →a 〈δ′ ,⃗aa〉, R(δ′ ,⃗aa), then R(δ,⃗a).

We also define a low-level program that represents all refinements of all high-level exogenous actions:

i.e., do any refinement of an exogenous high-level primitive action,

where setp(P) a "delayed commitment" nondeterministic branch construct that executes a set of programs P nondeterministically without committing to which element of P is being executed until it has to. 9

Given this, we can state our assumption:

Assumption 7 (Exogenous HL Actions Never Diverge)

For all ground high-level action sequences ⃗α and all ground low-level action sequences ⃗a such that 〈m(⃗α), ϵ〉 →∗ ⃗a 〈δl,⃗a〉 and 〈δl,⃗a〉✓ for some δl, if there exists a ground high-level exogenous action β ∈ Ae such that Dl∪C∪Sensed(⃗a)∪{∃s.Do(m(β), do(⃗a, S0), s} is satisfiable, then we have that NecTerminates(ANYONEEXOHL,⃗a).

9 [Banihashemi et al., 2018b] axiomatize setp(P) as follows:

T rans(setp(P ), s, δ′ , s′ ) ≡

∃δ.∃δ′′ .δ ∈ P ∧ T rans(δ, s, δ′′ , s′ ) ∧

δ′ = setp({δ′′ | ∃δ.δ ∈ P ∧ Trans(δ, s, δ′′ , s′ )})

F inal(setp(P ), s) ≡ ∃δ.δ ∈ P ∧ F inal(δ, s).

These assumptions together with Dh being a sound abstraction of Dl wrt mapping m allow us to show our main result, i.e., if the high-level agent has a strategy γh to successfully execute a task represented by δh, then there exists a low-level strategy γl such that the low-level agent can ensure successful execution of a refinement of γh by using strategy γl, a refinement of γh; moreover, if it is known at the high level that after successful execution of δh, a situationsuppressed formula φ holds, then every such γl, ensures that the refinement of φ holds after γl terminates:

Theorem 3 (Strategy Refinement) Suppose that Dh is a sound abstraction of Dl relative to mapping m and that Assumptions 1 to 7 hold. Then for all ground high-level action sequences ⃗α and all ground low-level action sequences ⃗a such that 〈⃗α, ϵ〉 →∗⃗α 〈δ′h , ⃗α〉 for some δ′h and 〈δ′h , ⃗α〉✓ and 〈m(⃗α), ϵ〉 →∗ ⃗a 〈δl,⃗a〉 and 〈δl,⃗a〉✓ for some δl and for any online situation-determined high-level program δh and high-level strategy γh such that AbleBy(δh, ⃗α, γh), we have that: 10

1. there exists a low-level strategy γl such that AbleBy(mp(γh), ⃗a, γl);
2. moreover, for any situation-suppressed formula φ, if Dh ∪ C |= ∀s.Do(δh, do(⃗α, S0), s) ⊃ φ[s] then AbleBy(mp(γh); m(φ)?, ⃗a, γl).

Part 1 is proven by induction on the length of the high-level strategy γh (i.e., number of actions in the longest branch), using Assumption 6 when γh starts with an ordinary action and Assumption 7 when it starts with (a set of) exogenous actions. Part 2 follows from Part 1, properties of AbleBy, and results on mp from [Banihashemi et al., 2018b]. Furthermore, it is clear from our proof that the low-level strategy γl can be obtained piecewise/incrementally: first obtain a refinement of the first step of γh, execute it online, and then repeat this for the remainder of γh until done.

Example 5 As discussed in Example 4, our agent has a highlevel strategy γh1 by which she can execute the task δh1 and achieve the goal φh1. Based on Theorem 3, there exists a lowlevel strategy γl1 by which the agent is able to accomplish a refinement of the goal m(φh1); in fact we have

γl1 = qryAM(C1); qryPr(C1); set( (repAM(C1, 1); repP r(C1, 1); selF lt(C1, Bz, F 1); pay(C1, Bz, F 1); nil), (repAM(C1, 1); repP r(C1, 0); selF lt(C1, Bz, F 1); pay(C1, Bz, F 1); nil), (repAM(C1, 0); repP r(C1, 1); selF lt(C1, Bz, F 1); pay(C1, Bz, F 1); nil), (repAM(C1, 0); repP r(C1, 0); selF lt(C1, Eco, F 1); pay(C1, Eco, F 1); nil))

where action qryAM(c) (resp. qryPr(c)) queries if air miles (resp. promotion) exist for customer c and repAM(c, x)

10 [Banihashemi et al., 2018b] extend the mapping m to a mapping mp that maps any SD high-level program δh to a SD low-level program that implements it: mp(δh ) .= setp({δh [A(⃗t)/atomic(m(A(⃗t))) for all A ∈ A, and F(⃗t)/m(F(⃗t)) for all F ∈ F]}), where atomic(δ) performs δ as an atomic unit, without allowing interleaving.

(resp. repPr(c, x)) is an exogenous action that informs the agent whether AirMiles(c) (resp. Promotion(c)) holds.

8 Conclusion

In this paper, we showed that abstraction can be used to make reasoning about ability much easier, even for agents that operate online, i.e., acquire new information as they execute. Specifically, we showed that under some reasonable assumptions, if the agent has a strategy by which she is able to achieve a goal at the high level, then we can refine it piecewise into a low-level strategy to achieve the refinement of the goal. Also, we identified general sufficient conditions for soundness of an abstraction to persist when the agent acquires new information.

The framework developed in this paper is very general and handles arbitrary first-order representations of the states of the dynamic systems. In such a general setting not much can be said about the computational aspects. However note that it is indeed possible to get an effective setting from the computational point of view if we restrict, for example, the high level to be propositional. In this way we get a finite state abstract system on which doing conditional planning becomes effective, (under the assumption that we are able to compute refinement of atomic actions). Similar results can be obtained for first-order bounded action theories [De Giacomo et al., 2016]. We leave these questions for future work.

Developing methodologies and (partially) automated techniques for obtaining sound abstractions are important topics for future work. [Banihashemi et al., 2017] shows that verifying that a number of properties are entailed by the low-level theory is sufficient to guarantee that one has a sound abstraction. Some of our assumptions are also straightforward entailment checks. For the others, we will investigate techniques for verifying them. Of course, one also needs to impose restrictions on the theory to get decidability as discussed above.

Acknowledgments

We acknowledge the support of Sapienza Ateneo Project Immersive Cognitive Environments and the National Science and Engineering Research Council of Canada.