Abstraction of Nondeterministic Situation Calculus Action Theories

1 Introduction

When working in realistic dynamic domains, the use of abstraction has proven essential in many areas of artificial intelligence, for example, in improving the efficiency of planning (e.g., [Chen and Bercher, 2021]), explaining agents' behavior (e.g., [Seegebarth et al., 2012]), and in reinforcement learning (e.g., [Sutton et al., 1999]).

Recently, [Banihashemi et al., 2017] (BDL17) proposed a formal account of 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 refinement mapping specifies how each high-level action is implemented by a low-level ConGolog program and how each high-level fluent can be translated into a low-level state formula. This work defines notions of abstractions between such action theories in terms of the existence of a suitable bisimulation relation

[Milner, 1971] between their respective models. 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. The framework can also be used to generate high-level explanations of low-level behavior.

This framework was formulated assuming a deterministic environment, as usual in the situation calculus. Hence, the only nondeterminism was coming from ConGolog programs and was angelic in nature, i.e., under the control of the agent [Levesque et al., 1997; De Giacomo et al., 2000].

However, many agents operate in nondeterministic environments where the agent does not fully control the outcome of her actions (e.g., flipping a coin where the outcome may be heads or tails). Recently, [De Giacomo and Lesp´erance, 2021] (DL21) proposed a simple and elegant situation calculus account of nondeterministic environments where they clearly distinguish between the nondeterminism associated with agent choices and that associated with environment choices, the first being angelic for the agent, and the second being devilish, i.e., not under the agent's control. 1 The presence of environment nondeterminism deeply influences reasoning about action: if the agent wants to complete a task, she cannot simply do standard logical reasoning (i.e., satisfiability/logical implication), but needs to do realizability/synthesis, i.e., devise a strategy that, in spite of the uncontrollable reactions of the environment, guarantees successful completion of the task [Church, 1963; Pnueli and Rosner, 1989; Abadi et al., 1989]. We see this, for example in planning, where in the classical deterministic setting the problem can be solved by heuristic search, while in fully observable nondeterministic (FOND) domains forms of adversarial (AND/OR) search are required [Cimatti et al., 1998; Haslum et al., 2019].

In this paper, we develop an account of agent abstraction in presence of nondeterministic environments based on (DL21). The refinement mapping between high-level fluents and lowlevel state formulas remains as in (BDL17). Instead we consider each high-level action, now nondeterministic, as being composed of an agent action and an (implicit) environment reaction. As a consequence, we map the agent action (without the environment reaction) into a low-level agent program that appropriately reflects the nondeterminism of the environment, and the complete high-level action, including both the agent action and the environment reaction, into a low-level system program that relates the high-level environment reaction to the low-level ones.

1 Earlier accounts dealing with the topic in the situation calculus were more complex and did not clearly distinguish between these two forms of nondeterminism, e.g., [Pinto et al., 2000] which deals with stochastic actions, and [Bacchus et al., 1999] which deals with uncertainty, noisy acting, and noisy sensing.

We show that the (BDL17) notion of m-bisimulation extends naturally to this new setting. This allows for exploiting abstraction when reasoning about executions as in (BDL17), in spite of the nondeterministic environment. But, notably, this new setting now supports strategic reasoning and strategy synthesis, by allowing us to quantify separately on agent actions and environment reactions. As a result, we can exploit abstraction by finding abstract strategies at the high-level and then refine them into concrete low-level ones. In particular, we show that if the agent has a (strong FOND) plan/strategy to achieve a goal/complete a task at the high level (i.e., no matter what the environment does), and she can always execute the nondeterministic high-level actions to completion at the low level (even if not controlling their outcome), then there exists a refinement of it that is a (strong FOND) plan/strategy to achieve the refinement of the goal/task at the low level.

2 Preliminaries

Situation calculus. The situation calculus is a well known predicate logic language for representing and reasoning about dynamically changing worlds [McCarthy and Hayes, 1969; Reiter, 2001]. All changes to the world are the result of actions, which are terms in the language. A possible world history is represented by a term called a situation. The constant S0 is used to denote the initial situation. Sequences of actions are built using the function symbol do, such that do(a, s) denotes the successor situation resulting from performing action a in situation s. Predicates and functions whose value varies from situation to situation are called fluents, and are denoted by symbols taking a situation term as their last argument (e.g., Open(Door1, s)). The abbreviation do([a1, . . . , an], s) stands for do(an, do(an-1, . . . , do(a1, s) . . .)); for an action sequence ⃗a, we often write do(⃗a, s) for do([⃗a], s). In this language, a dynamic domain can be represented by a basic action theory (BAT), where successor state axioms represent the causal laws of the domain and provide a solution to the frame problem [Reiter, 2001]. A special predicate Poss(a, s) is used to state that action a is executable in situation s; the precondition axioms characterize this predicate. Abbreviation Executable(s) means that every action performed in reaching situation s was possible in the situation in which it occurred.

Nondeterministic situation calculus. A major limitation of the standard situation calculus and BATs is that atomic actions are deterministic. [De Giacomo and Lesp´erance, 2021] (DL21) propose a simple extension of the framework to handle nondeterministic actions while preserving the solution to the frame problem. For any primitive action by the agent in a nondeterministic domain, there can be a number of different outcomes. (DL21) takes the outcome as being determined by the agent's action and the environment's reaction to this action. This is modeled by having every action type/function A(⃗x, e) take an additional environment reaction parameter e, ranging over a new sort Reaction of environment reactions. The agent cannot control the environment reaction, so it performs the reaction-suppressed version of the action A(⃗x) and the environment then selects a reaction e to produce the complete action A(⃗x, e). We call the reaction-suppressed version of the action A(⃗x) an agent action and the full version of the action A(⃗x, e) a system action.

Nondeterministic basic action theories (NDBATs). These can be seen as a special kind of BAT, where every action function takes an environment reaction parameter, and moreover, for each agent action A(⃗x), we

• have its agent action precondition denoted by: Possag(A(⃗x), s) .= φagPoss A (⃗x, s);
• have a reaction independence requirement, stating that the precondition for the agent action is independent of any environment reaction: ∀e.Poss(A(⃗x, e), s) ⊃ P ossag (A(⃗x), s);
• have a reaction existence requirement, stating that if the precondition of the agent action holds then there exists a reaction to it which makes the complete system action executable: Possag(A(⃗x), s) ⊃ ∃e.Poss(A(⃗x, e), s).

The above requirements must be entailed by the action theory for it to be an NDBAT.

A NDBAT D is the union of the following disjoint sets: foundational, domain independent, axioms of the situation calculus (Σ) as in standard BATs, axioms describing the initial situation DS0 as in standard BATs, unique name axioms for actions (Duna) as in standard BATs, successor state axioms (SSAs) describing how fluents change after system actions are performed (Dssa), and system action precondition axioms, one for each action type, stating when the complete system action can occur (Dposs); these are of the form: P oss(A(⃗x, e), s) ≡ φP oss A (⃗x, e, s).

Example. Our running example is based on a triangle tireworld domain (see Fig. 1). The agent's goal is to drive from location 11 to location 13. When driving from one location to the next, the possibility of a tire going flat exists. If there is a spare tire in the location where the car is at (indicated by circles in Fig. 1), the agent can use it to fix a flat.

NDBAT Dtt l models the domain at the low level. The system action drive(o, d, r) can be performed by the agent to drive from origin location o to destination location d, and r indicates environment's reaction. This action is executable when the agent action drive(o, d) is executable (i.e., when the agent is at o, a road connects o to d, and agent does not have a flat tire), and r can take on two values: FlatTire if the tire goes flat and NoFlatTire otherwise. The fluent AtLL(l, s) indicates agent's location, RoadLL(o, d, s) specifies the road connections in Fig. 1, FlatLL(s) describes whether there is a flat tire, and VisitedLL(l, s) indicates if the location l has already been visited by the agent.

The system action fixFlatTire(l, r) fixes a flat tire, and the environment reaction r is SuccessLF (assumed for simplicity). It is executable if the fluent SpareLL(l, s) holds, i.e., there is a spare tire. The action waitLL can be performed by the agent to remain idle at a location.

Dtt l includes the following action precondition axioms (throughout the paper, we assume that free variables are universally quantified from the outside):

Possag(drive(o, d), s) .= o ̸= d ∧ AtLL(o, s) ∧ RoadLL(o, d, s) ∧ ¬FlatLL(s) Possag(fixFlatTire(l), s) .= AtLL(l, s) ∧ SpareLL(l, s) ∧ FlatLL(s) Possag(waitLL, s) .= TRUE P oss(drive(o, d, r), s) ≡ P ossag(drive(o, d), s) ∧ (r = FlatTire ∨ r = NoFlatTire) P oss(fixFlatTire(l, r), s) ≡ P ossag(fixFlatTire(l), s) ∧ r = SuccessLF P oss(waitLL(r), s) ≡ P ossag(waitLL, s) ∧ r = SuccessLW

Dtt l also includes the following SSAs: AtLL(l, do(a, s)) ≡ ∃o, r.a = drive(o, l, r) ∨ AtLL(l, s) ∧ ∀d, r.a ̸= drive(l, d, r) FlatLL(do(a, s)) ≡ ∃o, d.a = drive(o, d, FlatTire) ∨ FlatLL(s) ∧ ∀r, l.a ̸= fixFlatTire(l, r) VisitedLL(l, do(a, s)) ≡ ∃o, r.a = drive(o, l, r) ∨ VisitedLL(l, s)

For the other fluents, we have SSAs specifying that they are unaffected by any action.

Dtt l also contains the following initial state axioms:

RoadLL(o, d, S0) ≡ (o, d) ∈ {(11, 12), (11, 21), (12, 21), (12, 22), (12, 13), (13, 22), (22, 31), (21, 31), (12, 11), (21, 11), (21, 12), (22, 12), (13, 12), (22, 13), (31, 22), (31, 21)}, SpareLL(l, S0) ≡ l ∈ {21, 22, 31}, VisitedLL(l, S0) ≡ l = 11, AtLL(l, S0) ≡ l = 11, DestLL(l, S0) ≡ l = 13, ¬FlatLL(S0).

FOND planning and synthesis in NDBATs. We start with some definitions. A weak plan is one that achieves the goal when the environment "cooperates" and selects environment reactions to nondeterministic actions that make this happen. Formally, we say that a sequence of agent actions ⃗a is a weak plan to achieve Goal if ∃s′ .Doag(⃗a, S0, s′ ) ∧ Goal(s′ ) holds, i.e., there exists an execution of ⃗a that takes us from the initial situation S0 to situation s′ where the goal holds. Doag(⃗a, s, s′ ) means that the system may reach situation s′ when the agent executes the sequence of agent actions ⃗a depending on environment reactions:

Doag(ϵ, s, s′ ) .= s′ = s (where ϵ is the empty sequence of actions) Doag([A(⃗x), σ], s, s′ ) .= ∃e.P oss(A(⃗x, e), s) ∧ Doag(σ, do(A(⃗x, e), s), s′ )

A strong plan for the agent guarantees the achievement of a goal no matter how the environment reacts; it is a strategy for the agent to follow to ensure that the goal is achieved. (DL21) define a strategy as a function from situations to (instantiated) agent actions. That is, f (s) = A(⃗t) denotes that the strategy f applied to situation s returns A(⃗t) as the next action to do. The special agent action stop (with no effects and preconditions) may be returned when the strategy wishes to stop. Given a strategy, we can check whether it forces the goal to become true in spite of the environment reactions, i.e., is a strong plan to achieve the goal. Formally, we have AgtCanForceBy(Goal, s, f), i.e., the agent can force Goal to become true by following strategy f in s:

AgtCanForceBy(Goal, s, f ) .= ∀P.[. . . ⊃ P(s)] where . . . stands for [(f (s) = stop ∧ Goal(s)) ⊃ P (s)]∧ [∃A.∃⃗t.(f (s) = A(⃗t) ̸= stop ∧ P ossag(A(⃗t), s)∧ ∀e.(P oss(A(⃗t, e), s) ⊃ P (do(A(⃗t, e), s)))) ⊃ P (s)]

We say that AgtCanForce(Goal, s) holds iff there is a strategy f such that AgtCanForceBy(Goal, s, f ) holds.

Example cont. Strategies use the stop action, hence we define a stopLL action at the low level; this action always terminates with the SuccessLS reaction. The strategy that guarantees reaching location 13 is defined as follows:

Dtt

l |= AgtCanForceBy(AtLL(13), S0, fl )

where

That is, the agent should stop if she is already at location 13, otherwise she drives to a location she has not visited before and that has a spare tire; in case of a flat tire, action fixFlatTire is executed; in all other cases the agent waits.

High-level programs and 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. Here we concentrate on (a variant of) ConGolog [De Giacomo et al., 2000] that includes the following constructs:

δ ::= α | ϕ? | δ1; δ2 | δ1|δ2 | πx.δ | δ∗ | δ1‖δ2

In the above, α is an action term, possibly with parameters, and ϕ is a 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 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. The construct if φ then δ1 else δ2 endIf is defined as [φ?; δ1] | [¬φ?; δ2]. We also use nil, an abbreviation for True?, to represents the empty program, i.e., when nothing remains to be performed.

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) F inal(δ, s), which holds if program δ may legally terminate in situation s. The definitions of Trans and F inal 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 as a legal terminating situation s′ , and is defined as Do(δ, s, s′ ) .= ∃δ′ .T rans∗ (δ, s, δ′ , s′ )∧F inal(δ′ , s′ ) where Trans∗ denotes the reflexive transitive closure of Trans. We use C to denote the axioms defining the ConGolog programming language.

For simplicity in this paper, we use a restricted class of ConGolog programs which are situation-determined (SD) [De Giacomo et al., 2012], i.e., for every sequence of actions, the remaining program is uniquely determined by the resulting situation:

SituationDetermined(δ, s) .= ∀s′ , δ′ , δ′′ . Trans∗ (δ, s, δ′ , s′ ) ∧ Trans∗ (δ, s, δ′′ , s′ ) ⊃ δ′ = δ′′

ConGolog program execution in ND domains. To specify agent behaviors in nondeterministic domains, (DL21) use ConGolog agent programs, which are composed as usual, but only involve agent (reaction-suppressed) atomic actions. The semantics for such agent programs is a variant of the one above where a transition for an atomic agent action may occur whenever there exists a reaction that can produce it.

Strategic reasoning in executing programs in ND domains. To represent the ability of the agent to execute an agent program in a ND domain (DL21) introduce AgtCanForceBy(δ, s, f ) as an adversarial version of Do in presence of environment reactions. This predicate states that strategy f, a function from situations to agent actions (including the special action stop), executes SD ConGolog agent program δ in situation s considering its nondeterminism angelic, as in the standard Do, but also considering the nondeterminism of environment reactions devilish/adversarial:

AgtCanForceBy(δ, s, f ) .= ∀P.[. . . ⊃ P(δ, s)] where . . . stands for [(f (s) = stop ∧ F inal(δ, s)) ⊃ P (δ, s)] ∧ [∃A.∃⃗t.(f (s) = A(⃗t) ̸= stop ∧ ∃e.∃δ′ .T rans(δ, s, δ′ , do(A(⃗t, e), s)) ∧ ∀e.(∃δ′ .T rans(δ, s, δ′ , do(A(⃗t, e), s))) ⊃ ∃δ′ .T rans(δ, s, δ′ , do(A(⃗t, e), s)) ∧ P (δ′ , do(A(⃗t, e), s)) ⊃ P (δ, s)]

We say that predicate AgtCanForce(δ, s) holds iff there exists a strategy f s.t. AgtCanForceBy(δ, s, f ) holds.

Example cont. Suppose we have a program δLL go (l) which lets the agent drive to any location, or fix a flat any number of times until a destination l is reached: δLL go (l) = (πo, d.drive(o, d) | πd.fixFlatTire(d))∗ ; AtLL(l)?

Now suppose the agent has been assigned the task of going to location 13. We can show that she has a strategy for executing the task δLL go (13):

Here, the strategy f to execute the task is same as fl above.

3 Abstraction in Nondeterministic Domains

In this section, we show how we can extend the agent abstraction framework of (BDL17) to handle nondeterministic domains. As in (BDL17), we assume that there is a highlevel/abstract (HL) action theory Dh and a low-level/concrete (LL) action theory Dl representing the agent's possible behaviors at different levels of detail. In (BDL17), these are standard BATs; here, we assume that they are both NDBATs. 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 ). The terms of sort Object are assumed be a countably infinite set N of standard names for which we have the unique name assumption and domain closure. We also assume that Reaction is a sub-sort of Object. Also, Dh and Dl are assumed to share no domain specific symbols except for the set of standard names for objects N. For simplicity and w.l.o.g., it is assumed that there are no functions other than constants and no non-fluent predicates.

Refinement mapping. As in (BDL17), we assume that one relates the HL and LL theories by defining a refinement mapping that specifies how HL atomic actions are implemented at the low level and how HL fluents can be translated into LL state formulas. In deterministic domains, one can simply map HL atomic actions to a LL program that the agent uses to implement the action. In nondeterministic domains however, we additionally need to specify what HL reaction the environment performs in each LL refinement of the HL action.

Definition 1 (NDBAT Refinement Mapping). A NDBAT refinement mapping m is a triple 〈ma, ms, mf 〉 where ma associates each HL primitive action type A in Ah to a SD ConGolog agent program δag A defined over the LL theory that implements the agent (i.e., reaction-suppressed) action, i.e., ma(A(⃗x)) = δag A (⃗x), ms associates each A to a SD ConGolog system program δsys A defined over the LL theory that implements the system action, i.e., ms(A(⃗x, e)) = δsys A (⃗x, e), thus specifying when the HL reaction occurs (system programs are interpreted using the standard transition semantics), and (as in (BDL17)) mf maps each situationsuppressed HL fluent F(⃗x) in Fh to a situation-suppressed formula φF (⃗x) defined over the LL theory that characterizes the concrete conditions under which F(⃗x) holds in a situation, i.e., mf (⃗x) = φF (⃗x).

We can extend a mapping to a sequence of agent actions in the obvious way, i.e., ma(α1, . . . , αn) .= ma(α1); . . . ;ma(αn) for n ≥ 1 and ma(ϵ) .= nil, and similarly for sequences of system actions. Note that ma(⃗α) is well defined even if the action parameters are not ground; but the action functions must be given. We also extend the notation so that mf(φ) stands for the result of substituting every fluent F (⃗x) in situation-suppressed formula φ by mf (F (⃗x)).

Agent actions and system actions must be mapped in a consistent way. To ensure this, we require the following:

Constraint 2. (Proper Refinement Mapping)

For every high-level system action sequence ⃗α and every high-level action A, we have that:

This ensures that (1) for every situation s′ that can be reached from s by executing a refinement of the HL agent action A(⃗x), there is a HL reaction e that generates it, and (2) that for every situation s′ that can be reached from s by executing a refinement of the HL system action A(⃗x, e), there is a refinement of the HL agent action that generates it (in the above, s is any situation reached by executing a sequence of HL system actions). Note that (1) essentially states that the reaction existence requirement holds at the low level for refinements of HL actions and (2) amounts to having the reaction independence requirement hold. We say that an NDBAT refinement mapping m is proper wrt low-level NDBAT Dl if this constraint holds.

Example cont. NDBAT Dtt h abstracts over driving and fixing potential flat tires. Action driveAndTryFix(o, d, r) can be performed to drive from origin o to destination d, and fix a flat if one occurs and a spare is available. This action is executable when driveAndTryFix(o, d) is executable, i.e., when the agent is at o, a road connects o to d, and agent does not have a flat tire; the environment reaction r may take on the following values: DrvNoFlat, if the tire does not go flat, DrvFlat if the tire goes flat and it is not possible to fix it, or DrvFlatFix if the tire went flat and the flat was fixed. Action waitHL lets the agent remain idle at a location. Dtt h includes the following system and agent action precondition axioms:

Possag(driveAndTryFix(o, d), s) .= o ̸= d ∧ AtHL(o, s) ∧ RoadHL(o, d, s) ∧ ¬FlatHL(s) Possag(waitHL, s) .= TRUE P oss(driveAndT ryF ix(o, d, r), s) ≡ P ossag (driveAndTryFix (o, d), s) ∧ (r = DrvNoFlat ∨ ¬SpareHL(d, s) ∧ r = DrvFlat ∨ SpareHL(d, s) ∧ r = DrvFlatFix ) P oss(waitHL(r), s) ≡ P ossag(waitHL, s) ∧ r = SuccessHW Dtt h also includes the following SSAs: AtHL(l, do(a, s)) ≡ ∃o, r.a = driveAndTryFix (o, l, r) ∨ AtHL(l, s) ∧ ∀d, r.a ̸= driveAndTryFix (l, d, r) FlatHL(do(a, s)) ≡ ∃o, d.a = driveAndTryFix(o, d,DrvFlat) ∨FlatHL(s) VisitedHL(l, do(a, s)) ≡ ∃o, r.a = driveAndTryFix (o, l, r) ∨ VisitedHL(l, s)

For the other fluents, we have SSAs specifying that they are unaffected by any action.

The initial state axioms of Dtt h are same as Dtt l , with highlevel fluents having a distinct name (with HL suffix); e.g., RoadHL is axiomatized exactly as RoadLL.

We specify the relationship between the HL and LL NDBATs through the following refinement mapping mtt :

mtt a (driveAndTryFix (o, d)) = drive(o, d); if ¬FlatLL then nil else if¬SpareLL(d) then nil else fixFlatTire(d) endIf endIf mtt a (waitHL) = waitLL mtt s (driveAndTryFix (o, d, rh)) = πrl.drive(o, d, rl); if ¬FlatLL then rh = DrvNoF lat? else if¬SpareLL(d) then rh = DrvFlat? else fixFlatTire(d, SuccessLF ); rh = DrvFlatFix ? endIf endIf mtt s (waitHL(rh)) = πrl.waitLL(rl); rh = SuccessHW? mtt f (FlatHL) = FlatLL

Thus, the HL agent action driveAndTryFix(o, d) is implemented by an LL program where the agent first performs drive(o, d), and depending on whether the tire has gone flat and a spare exists at location d, fixes the tire or does nothing. Fluents AtHL(l), SpareHL(l), RoadHL(o, d), DestHL(l), and VisitedHL(l) are mapped to their low-level counterparts similar to FlatHL. We can show that: 2

Proposition 3. NDBAT refinement mappingmtt is proper wrt Dtt l .

m-Bisimulation. To relate the HL and LLmodels/theories, (BDL17) define a variant of bisimulation [Milner, 1971; Milner, 1989]. 3 The base condition for the bisimulation is:

Definition 4 (m-isomorphic situations). Let Mh be model of the HL theory Dh, and Ml a model of the LL theory Dl ∪ C. We say that situation sh in Mh is m-isomorphic to situation sl inMl, written sh ∼Mh,Ml m sl, if and only if

for every high-level primitive fluent F(⃗x) in Fh and every variable assignment v.

If sh ∼Mh,Ml m sl, then sh and sl evaluate all HL fluents the same.

Definition 5 (m-Bisimulation). Given Mh a model of Dh, 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 m-bisimulation relation between Mh and Ml if 〈sh, sl〉 ∈ B implies that: (i) sh ∼Mh,Ml m sl; (ii) for every HL primitive action type A in Ah, if there exists s′h such that Mh, v[s/sh, s′ /s′h ] |= Poss(A(⃗x), s) ∧ s′ = do(A(⃗x), s), then there exists s′l such that Ml, v[s/sl, s′ /s′l ] |= Do(m(A(⃗x)), s, s′ ) and 〈s′h , s′l 〉 ∈ B; and (iii) for every HL primitive action type A in Ah, if there exists s′l such that Ml, v[s/sl, s′ /s′l ] |= Do(m(A(⃗x)), s, s′ ), then there exists s′h such that Mh, v[s/sh, s′ /s′h ] |= Poss(A(⃗x), s) ∧ s′ = do(A(⃗x), s) 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.

2 For proofs, see [Banihashemi et al., 2023]

3 As usual, M, v |= φ means that model M and assignment v satisfy formula φ (where φ may contain free variables that are interpreted by v); also v[x/e] represents the variable assignment that is just like v but assigns variable x to entity e.

The definition of m-bisimulation can remain as in (BDL17) where conditions (ii) and (iii) are applied to highlevel system primitive actions and their mapping ms.

The definition of m-bisimulation ensures that performing a HL system action results in m-bisimilar situations. We can show that with the restriction to proper mappings, this automatically carries over to HL agent actions (so there is no need to change the definition of m-bisimulation to get this):

Theorem 6. Suppose that Mh ∼m Ml, where Mh |= Dh, Ml |= Dl ∪C, Dh and Dl are both NDBATs, and m is proper wrt Dl. Then for any HL system action sequence ⃗α and any HL primitive action A, we have that:

1. if there exist sh and s′h such that Mh, v[s/sh, s′ /s′h ] |= Do(⃗α, S0, s)∧Doag(A(⃗x), s, s′ ), then there exist sl and s′l such that Ml, v[s/sl, s′ /s′l ] |= Do(ms(⃗α), S0, s) ∧ Doag(ma(A(⃗x)), s, s′ ), sh ∼Mh,Ml m sl, and s′h ∼Mh,Ml m s′l ;
2. if there exist sl and s′l such that Ml, v[s/sl, s′ /s′l ] |= Do(ms(⃗α), S0, s) ∧Doag(ma(A(⃗x)), s, s′ ), then there exist sh and s′h such that Mh, v[s/sh, s′ /s′h ] |= Do(⃗α, S0, s) ∧ Doag(A(⃗x), s, s′ ), sh ∼Mh,Ml m sl, and s′h ∼Mh,Ml m s′l .

(BDL17) use m-bisimulation to define notions of sound/complete abstraction between a high-level action theory and a low-level one: 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 such that Mh ∼m Ml. With a sound abstraction, whenever the highlevel 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 is satisfiable, then the high level does also. 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, there exists a model Ml of Dl ∪ C such that Ml ∼m Mh.

The notion of m-bisimulation provides the semantic underpinning of these notions of abstraction. (BDL17) also prove the following results that identify a set of properties that are necessary and sufficient to have a sound/complete abstraction (here we adjust the notation to use system actions) and can be used to verify that one has a sound/complete abstraction, e.g., by model checking or theorem proving techniques:

Theorem 7 (BDL17). Dh is a sound abstraction of Dl relative to mapping m if and only if for any sequence of high-level system actions ⃗α:

• (a) DlS0 ∪Dlca ∪Dlcoa |=mf(φ), for all φ ∈ Dh S0 ,

where φPoss Ai (⃗x, rh) is the right hand side (RHS) of the precondition axiom for system action Ai(⃗x, rh), and φssa Fi,Ai (⃗y, ⃗x, rh) is the RHS of the successor state axiom for Fi instantiated with system action Ai(⃗x, rh) where action terms have been eliminated using Dh ca .

Theorem 8 (BDL17). If Dh is a sound abstraction of Dl relative to mapping m, then Dh is also a complete abstraction of Dl wrt mapping m if and only if for every model Mh of Dh S0 ∪Dh ca ∪Dh coa , there exists a model Ml of DlS0 ∪Dlca ∪Dlcoa such that SMh 0 ∼Mh,Ml m SMl 0 .

Using the above results, we can show that:

Proposition 9. Dtt h is a sound and complete abstraction of Dtt l wrt mtt .

Note that in this paper, we are focusing on fully observable domains, so we will just present results about m-bisimilar NDBAT models; Mh ∼m Ml essentially means that Mh is a sound and complete abstraction of Ml relative to m.

4 Results about Action Executions

We now show some interesting results about the use of NDBAT abstractions to reason about action executions. Our results will be mostly about m-bisimilar NDBAT models, i.e., where Mh ∼m Ml; unless stated otherwise, we assume we have NDBATs Dh and Dl, that Mh |= Dh ∪ C and Ml |= Dl ∪ C, and that m is proper wrt Dl.

Firstly, we have that m-isomorphic situations satisfy the same high-level situation-suppressed formulas:

Lemma 10 (BDL17). If sh ∼Mh,Ml m sl, then for any highlevel situation-suppressed formula φ, we have that:

Secondly, we can show that in m-bisimilar models, the same sequences of high-level system actions are executable, and that in the resulting situations, the same high-level situation-suppressed formulas hold:

Theorem 11. If Mh ∼m Ml, then for any sequence of high-level system actions ⃗α and any high-level situationsuppressed formula φ, we have that

Here and below, sequences of high-level system actions ⃗α may contain free variables in the action parameters, but the action functions must be given, and similarly for sequences of high-level agent actions (this generalizes (BDL17) which only considers ground action sequences).

We can extend this result to sequences of agent actions by exploiting the fact that m is a proper mapping:

Theorem 12. If Mh ∼m Ml, then for any sequence of highlevel agent actions ⃗α and any high-level situation-suppressed formula φ, we have that

This means that if the agent has a weak plan to achieve a goal at the high level, then there exists a refinement of it that is a weak plan to achieve the mapped goal at the low level.

Example cont. At the high level, a weak plan to achieve the goal of getting to location 13 is to first drive to 12 and then to 13:

This plan works provided no flat occurs when driving to 12, as there is no spare there. By Th. 12, there exists a weak plan at the low level that refines this high-level plan:

5 Results about Strategic Reasoning

Let us now discuss how NDBAT abstractions can be used in FOND domains to synthesize strategies to fulfill reachability/achievement goals as well as temporally extended goals/tasks. First of all, we need to consider how much strategic reasoning the agent needs to do to execute a high-level atomic action at the low level. A given HL agent action A(⃗x) is mapped to a LL agent programma(A(⃗x)) that implements it. As we have seen, in m-bisimilar models, Constraint 2 ensures that if A(⃗x) is executable at the HL, then there exists a terminating execution of ma(A(⃗x)) at the LL (this holds for HL system actions as well). But this does not mean that all executions of ma(A(⃗x)) terminate, as some may block or diverge, due to either agent or environment choices. In general, the agent must do strategic reasoning to ensure that the execution of ma(A(⃗x)) terminates (and the environment may need to cooperate as well). But we can impose further constraints on the mapping of HL actions to avoid this or ensure that a strategy exists. Note that ensuring that the execution of ma(A(⃗x)) terminates does not mean that the agent controls the action's outcome (e.g., not having a flat); the outcome is still determined by the environment reactions.

Constraints onHL action implementation. First, we may want to require that the mapping of HL actions is such that the implementation program always terminates and no LL strategic reasoning is required to ensure termination. To do this, we first define:

InevTerminates(δ, s) .= ∀P.[. . . ⊃ P(δ, s)] where . . . stands for [(F inal(δ, s)) ⊃ P (δ, s)]∧ [∃s′ .∃δ′ .T rans(δ, s, δ′ , s′ )∧ ∀s′ .∀δ′ .(T rans(δ, s, δ′ , s′ ) ⊃ P (δ′ , s′ )) ⊃ P (δ, s)]

InevT erminates(δ, s) means that program δ executed starting in situation s inevitably terminates , i.e., all its executions eventually terminate. 4

Then we can ensure that for any HL agent action that is possibly executable at the low level, all executions terminate (i.e., they never block or diverge) by requiring the following:

4 This is analogous to the CTL [Clarke and Emerson, 1981] formula AFφ, i.e., on all paths eventually φ.

Constraint 13. (HL actions Inevitably Terminate) For every high-level system action sequence ⃗α and every high-level action A, we have that:

Dl ∪ C |= ∀s.(Do(ms(⃗α), S0, s) ⊃ ∀⃗x.(∃s′ .Doag(ma(A(⃗x)), s, s′ ) ⊃ InevT erminates(ma(A(⃗x)), s)))

Proposition 14. NDBAT Dtt l and mapping mtt satisfy Constraint 13.

If we impose Constraint 13, then the agent that executes the program that implements the HL action can be a dumb executor. But this may seem too restrictive. An alternative is to impose the weaker requirement that for any HL agent action that is possibly executable at the LL, the agent has a strategy to execute it to termination no matter how the environment reacts (even if not controlling its outcome). Formally:

Constraint 15. (Agt Can Always Execute HL actions) For every high-level system action sequence ⃗α and every high-level action A, we have that:

Note that if we only impose Constraint 15, then there is no guarantee that when a HL system action A(⃗x, e) is possibly executable, the environment can actually ensure that reaction e occurs when the agent executes ma(A(⃗x)). We can define an additional constraint that ensures this; see [Banihashemi et al., 2023] for details.

Planning for achievement goals. Returning to planning, we can now show that if Constraint 15 holds (i.e., the agent always knows how to execute high-level primitive actions at the low level, even if not controlling their outcome) and the agent has a strong plan to achieve a goal at the high level, then there exists a refinement of the high-level plan that is a strong plan to achieve the refinement of the goal at the low level:

Theorem 16. If Mh ∼m Ml and Constraint 15 holds, then for any high-level system action sequence ⃗α and any highlevel situation-suppressed formula φ, we have that:

if Mh, v |= Executable(do(⃗α, S0)) ∧ AgtCanF orce(φ, do(⃗α, S0)) then Ml, v |= ∃s.Do(ms(⃗α), S0, s) ∧ ∀s.Do(ms(⃗α), S0, s) ⊃ AgtCanF orce(mf (φ), s)

Proof sketch. The proof is by induction on the length of the HL strategy fh at do(⃗α, S0), where the length of a strategy is the length of its longest branch, i.e., length(f, s) .= 0 if f(s) = stop and length(f, s) .= maxDoag(f(s),s,s′ )(length(f, s′ )) otherwise.

Assume the antecedent. It follows that there is a strategy fh such that AgtCanForceBy(φ, sh, fh), where sh = do(⃗α, S0). By proof of Theorem 11 we have that at the LL ∃sl.Do(ms(⃗α), S0, sl) and for all such sl we have that sh ∼Mh,Ml m sl. Take an arbitrary such sl. We show that there exists a LLl strategy fl such that AgtCanF orceBy(mf (φ), sl , fl).

Base case, when length(fh, sh) = 0, and fh(sh) =

stop ∧ φ[sh]. By Lemma 10, we have that mf(φ)[sl] and AgtCanForceBy(mf (φ), sl, fl ) for any strategy fl such that fl (sl) = stop.

Inductive case: Assume the result holds for any HL strategy fh of length at most k. We show that it must also hold for a HL strategy fh of length k + 1.

At the HL, by the definition of AgtCanForceBy, we have that there exists an high-level action A(⃗t) such that fh(sh) =

∀s′h .Doag(A(⃗t), sh, s′h ) ⊃ AgtCanF orceBy(φ, s′h , fh ).

By Constraint 15, there exists a LL strategy gl such that AgtCanForceBy(ma(A(⃗t)), sl, gl). For any s′l such that Doag(gl, sl, s′l ), it follows by Constraint 2 that there exists s′h such that s′h ∼Mh,Ml m s′l . The length of fh at s′h is at most k. Thus by the induction hypothesis, there exists a LL strategy f ′ l such that AgtCanForceBy(mf(φ), s′l , f ′ l ). It follows that AgtCanForceBy(mf (φ), sl, fl ) for fl = f ′ l ◦ gl.

Example cont. As strategies use the stop action, we first define a stopHL action at the high level which is mapped to the stopLL action at the concrete level; stopHL always terminates with the SuccessHS reaction. By Proposition 14, Constraint 13 (and thus also the weaker Constraint 15) is satisfied for our example domain.

We can show that the agent has a strong plan to achieve the goal of being at location 13 at the high level (dtf abbreviates driveAndT ryF ix):

The agent's high-level strategy fh is to stop if she is already at location 13, otherwise to drive to a location which has not been visited previously and has a spare tire and fix a flat if one occurs; in all other cases she waits.

By Th. 16 there exists a strategy at the low level that is refinement of the high-level strategy; this strategy is the same as strategy fl in Section 2. It is easy to show that fl is a refinement of the high-level strategy fh.

Planning for temporally extended goals/tasks. We can also show a similar result to the previous theorem for highlevel programs/tasks/temporally extended goals: if Constraint 15 holds and the agent has a strategy to successfully execute an agent program (without concurrency) at the high level, then the agent also has a strategy to successfully execute some refinement of it at the low level:

Theorem 17. If Mh ∼m Ml and Constraint 15 holds, then for any high-level system action sequence ⃗α and any SD ConGolog high-level agent program δ without the concurrent composition construct, we have that:

if Mh, v |= Executable(do(⃗α, S0)) ∧ AgtCanF orce(δ, do(⃗α, S0)) then Ml, v |= ∃s.Do(ms(⃗α), S0, s) ∧ ∀s.Do(ms(⃗α), S0, s) ⊃ AgtCanF orce(ma(δ), s)

Here, we apply the mapping to a high-level agent program δ without concurrency to produce a low level agent program ma(δ); this can be defined in the obvious way, using ma to map atomic actions and mf for tests as usual, and by mapping the components and composing the result for other constructs, e.g., ma(δ1|δ2) = ma(δ1)|ma(δ2) (we discuss concurrency in [Banihashemi et al., 2023]).

Proof sketch. The proof is by induction on the length of the high-level strategy fh for executing δ at do(⃗α, S0) and is similar to that of the above theorem. Note that since δ is SD, does not involve concurrency, and the high-level atomic actions are all mapped to SD programs, ma(δ) must also be SD (we execute a high-level action using the appropriate strategy essentially as a procedure call and the high-level program continues after the call has completed).

Example cont. Consider the high-level program δHL go (l) = (πo, d.driveAndTryFix(o, d))∗ ;AtHL(l)? which goes to location l by repeatedly picking adjacent locations and doing driveAndTryFix(o, d) until the agent is at l. We can show that the agent has a strategy to successfully execute this program to get to location 13:

Here, the high-level strategy fh to execute the program is same as the one we saw above. It can also be shown that the low-level strategy fl seen earlier is a refinement of fh and can be used to to execute ma(δHL go (13)). To further illustrate the use of high-level programs, notice that we could give the agent the program δHL go (31); δHL go (13) to execute. This is a more complex task as she must first go to location 31 and then to 13; but it is easier to to find a strategy to do it.

In [Banihashemi et al., 2023], we show how we can handle more complex domains where reactions represent (sets of) exogenous actions.

6 Monitoring and Explanation

Being able to monitor what a low-level agent is doing and describe it in abstract terms (e.g., to a client or manager) is particularly important in the context of Explainable AI. (BDL17) show how a sound abstraction wrt a mapping m can be used to do this when certain conditions hold. They define an inverse mapping m-1 that takes a sequence of low-level actions ⃗a and returns the sequence of high-level actions ⃗α that it refines in a given model. In [Banihashemi et al., 2023], we show that we can easily adapt this approach for NDBAT abstractions.

Example cont. Consider a variant of our running example where, if the agent has a flat and there is no spare tire in a location (i.e., at locations 11, 12 and 13), she can either buy one, or she can use a roadside assistance service to get one provided the location is within the covered area, We can have HL actions for these with the mapping:

mtt+ s (buyAndFix(l, rh)) = πr.order(l, r); πr.pay(l, r); πr.fixFlatTire(l, r); rh = SuccHBuy? mtt+ s (serviceAndFix(l, rh)) = π.r.callServiceLL(l, r); πr.fixFlatTire(l, r); rh = SuccHServ?

Suppose that at the LL, the agent knows that both locations 12 and 13 fall under the roadside service coverage, while at the HL, the agent only knows this for 13 (we have imperfect information). We can define NDBATs for this and show Dtt+ h is a sound abstraction of Dtt+ l [Banihashemi et al., 2023].

Now suppose that at the LL, the sequence of system actions ⃗a = drive(11, 21,NoFlatTire); drive(21, 12, FlatTire) has occurred. In location 12, no spare tire is available, and if the agent wants to move on with her journey, she needs to either call for service or order a new tire. The inverse mapping tells us that HL system action sequence ⃗α = driveAndTryFix(11, 21,DrvNoFlat); driveAndTryFix(21, 12,DrvFlat) has occurred. Since Dtt+ h |= AtHL(12, do(⃗α, S0)), we can conclude at the HL that the agent is now at location 12. Since Dtt+ h ∪{Poss(serviceAndFix(12, SuccHServ), do(⃗α, S0))} is satisfiable, we can also conclude that serviceAndFix(12, SuccHServ) might occur next, and similarly for buyAndFix(12, SuccHBuy); in fact we know at the HL that the latter is executable: Dtt+ h |= Poss(buyAndFix(12, SuccHBuy), do(⃗α, S0)).

7 Discussion

There has been much previous work on fully/partially observable nondeterministic planning, e.g., [Ghallab et al., 2004; Cimatti et al., 2003; Muise et al., 2014], strategy logics such as ATL [Alur et al., 2002], and strategic reasoning [Xiong and Liu, 2016b; Xiong and Liu, 2016a]. But such work assumes that the domain is represented at a single level of abstraction.

In planning, approaches such as hierarchical task networks (HTNs) [Erol et al., 1994] support abstract tasks that facilitate search. [Kuter et al., 2009] propose an algorithm which combines HTN-based search-control strategies with Binary Decision Diagram-based state representations for planning in nondeterministic domains. [Chen and Bercher, 2021] extend HTN planning with nondeterministic primitive tasks. [Bonet et al., 2017] investigate nondeterministic abstractions for generalized planning, where one looks for a (typically iterative) plan that solves a whole class of related planning problems. [Cui et al., 2021] applies the abstraction framework of (BDL17) to generalized planning. They use Golog programs to represent nondeterministic actions, and our results should make it possible to simplify their framework.

[Banihashemi et al., 2018] generalized the approach of (BDL17) to deal with agents that may acquire new knowledge during execution, and formalized (piecewise) hierarchical refinements of an agent's ability (i.e., strategy) to achieve a goal. However, this work does not consider nondeterministic actions and is based on a more complex framework involving online executions.

Abstraction is important for efficient reasoning and explainability. This paper presents foundational results, i.e., a generic framework for abstraction in nondeterministic domains, which can be used for many reasoning tasks, such as planning, execution monitoring, and explanation. One potential practical application area is smart manufacturing. For instance, [De Giacomo et al., 2022] present a "manufacturing as a service" framework where facilities (made up of concrete resources) bid to produce products, given an abstract product recipe, which is based on an abstract information model in the cloud. Our work shows how one can develop an abstract domain model where planning for arbitrary high-level goals is easier and where we have guarantees that a high-level plan can be refined into a low-level one. It also allows one to monitor the low-level system by generating high-level descriptions of low-level system executions from which one can reason at the high level about what might happen next. Note that often manufacturing processes depend on the data and objects (parts) they produce and consume; to formalize this aspect, the situation calculus which provides a first-order representation of the state of the processes can indeed be used. Another potential practical application area is business process management, to support execution monitoring, explanation, and failure handling, see e.g., [Marrella et al., 2017].

As discussed in Section 3, (BDL17) identifies a set of properties that are necessary and sufficient to have a sound/complete abstraction wrt a mapping, which can be used to verify that one has such an abstraction. This means that in the finite domain/propositional case, verifying that one has a sound abstraction is decidable and one can use theorem proving techniques to do it. Moreover, when one has complete information and a single model, one can use model-checking techniques. Bounded basic action theories [De Giacomo et al., 2016] constitute an important class of infinite domain theories where verification is decidable. In the general infinitedomain case, there are sound but incomplete reasoning methods that can be used [De Giacomo et al., 2010].

Automatically synthesizing sound/complete abstractions is another interesting problem. [Luo et al., 2020] show that one can use the well-explored notion of forgetting (of low-level fluent and action symbols) to automatically obtain a sound and complete high-level abstraction of a low-level BAT for a given mapping under certain conditions. They also show that such an abstraction is computable in the propositional case. However in general, there may be many different abstractions of a low-level theory, each of which may be useful for a different purpose. So defining an abstract language and mapping for a domain is not a trivial problem. Some human intervention is likely to be required, e.g., the modeler might specify the goals of the abstraction, or which details can be considered unimportant.

In this paper, we have not considered fairness constraints and strong cyclic plans [D'Ippolito et al., 2018; Aminof et al., 2020]; this is a topic for future work. Another interesting direction for future research is to consider a notion of multitier planning [Ciolek et al., 2020], where planning may be done using a simple model without unlikely contingencies, but where one can fall back to a more complex model when such contingencies do occur or more robustness is required. Related to this is the notion of "best effort strategies" (in presence of multiple [contradictory] assumptions about the environment) as proposed by [Aminof et al., 2021]. These are agent plans which, for each of the environment specifications individually, realize the agent's goal against a maximal set of environments satisfying that specification. We are also interested in extending the current framework to deal with partial observability and sensing.

Acknowledgments

Work supported by the ERC Advanced Grant WhiteMech (No. 834228), by the EU ICT-48 2020 project TAILOR (No. 952215), as well as by the National Science and Engineering Research Council of Canada.