An Operational Semantics for a Fragment of PRS

1 Introduction

The Procedural Reasoning System (PRS) [Georgeff and Ingrand, 1989; Georgeff and Lansky, 1987; 1986] is generally recognised as one of the first implementations of the BeliefDesire-Intention (BDI) [Bratman, 1987] model of agency and practical reasoning. PRS has been extremely influential, and is still widely used [Ghallab et al., 2016], particularly in robotics, e.g., [Ingrand et al., 1996; Alami et al., 1998; Foughali et al., 2016; Niemueller et al., 2017; Lemaignan et al., 2017]. For example, PRS-based systems secured first and second places in recent RoboCup and ICAPS logistics competitions. PRS has also influenced the design of many subsequent BDI-based agent programming languages, e.g., [Rao, 1996; Huber, 1999; Busetta et al., 1999; Winikoff et al., 2002; Morley and Myers, 2004; Sardina et al., 2006; Sardina and Padgham, 2011], though most of these languages implement only a subset of the programming language features supported by PRS. Surprisingly, given its centrality in the BDI paradigm, PRS lacks a formal operational semantics, which makes it difficult to determine its expressive power relative to other BDI agent programming languages, or to verify the correctness of PRS programs. For example, there is a widespread "folk belief" in the agent programming community that the plan graphs used by PRS are more expressive than most if not all other BDI agent formalisations, yet no proof of this intuition exists.

In this paper, we give a formal semantics for a significant fragment of PRS. We focus on language features specific to PRS, and in particular, its graph-based representation for plans and its programming constructs for maintaining a condition (i.e., maintenance goals). We make three main contributions. First, we develop a formalisation for the syntax of PRS as a directed bipartite graph (Section 2). Second, we provide an operational semantics that accounts for graph-based plans and adopting, suspending, resuming, and aborting (nested) maintenance goals (Section 3). Third, we prove key properties of the semantics of these PRS-specific programming constructs, and show that PRS plan-graphs are strictly more expressive than the plan rules found in typical BDI languages (Section 4). In Section 5, we briefly discuss related work and conclude.

2 PRS Syntax

We briefly recall the syntax and deliberation cycle of PRS, as defined in [Ingrand, 1991]. In the interests of brevity, we omit some features of the language, including meta-level reasoning, 'true concurrency', semaphores, and features such as 'if' and 'else' statements expressible in terms of the fragment we define. Plans in PRS consist of graphs. For compactness, and to allow a precise specification of the semantics, we adopt a plan-rule notation similar to that used in other BDIbased agent programming languages to specify the triggering and context conditions of plans, and specify plan bodies using a textual representation of bipartite graphs. We assume a first-order language with a vocabulary consisting of mutually disjoint and infinite sets of variable, constant, predicate, node, event-goal, and action symbols.

A PRS agent is defined by a belief base B, an action-library Λ, and a plan-library Π. A belief base is a set of ground atoms. An action-library is a set of action-rules specifying the actions available to the agent. An action is of the form act(⃗t), where act is an n-ary action symbol denoting an evaluable function that may change the agent's environment, and ⃗t = t1, . . . , tn are (possibly ground) terms. Actionrules are similar to STRIPS operators, and are of the form act(⃗v):ψ ← Φ+; Φ-, where ⃗v = v1, . . . , vn are variables; ψ is a formula specifying the precondition of the action; and the add-list Φ+ and delete-list Φ- are sets of atoms that specify the effects of executing the action. A plan-library Π consists of a set of plan-rules of the form e(⃗t):ϕ ; ψ ← G, where e is an n-ary event-goal symbol, ⃗t = t1, . . . , tn are terms, ϕ and ψ are formulas, and G is a plan-body graph. The rule states that, if the context condition ψ holds, G is a 'standard operating procedure' for achieving the event-goal e(⃗t) or the goal-condition ϕ.

Plan-body graphs are built from the following set of user programs: actions; belief addition +b adds the atom b to B; belief removal -b removes the atom b from B; test ?φ, where φ is a formula, tests whether φ holds in B; event-goal program or goal-condition program !ev, where ev ∈ {e, φ}, specifies that ev needs to be achieved; wait WT(φ) waits until formula φ holds in B; passive preserve PRp(!ev, φ) specifies that !ev needs to be achieved while monitoring φ and aborted if ev fails or φ does not hold; and active preserve PRa(!ev, φ), which is similar to the former except that if condition φ does not hold, the plan-body graph for !ev is suspended and the re-achievement of φ is attempted by posting the goal !φ. If the goal succeeds and φ is re-achieved then the active preserve is resumed, and otherwise it is aborted (if the goal fails) or re-suspended (if the goal succeeds but φ is still not achieved). Since user program !ev may generate subgoals, wait and preserve programs may also become 'nested' within one another, giving rise to potentially complex interactions. We use PRx(!ev, φ) to denote either PRa(!ev, φ) or PRp(!ev, φ). Formally, a user program Pu is a formula in the language defined by the grammar

A plan-body graph is a directed bipartite graph representing a partially ordered set of user programs, where the set of nodes (i.e., node symbols) is split into state nodes, and transition nodes initially labelled with the user programs.

Definition 1. Let Pu be the set of all user programs. A planbody graph G is a tuple 〈S , T , Ein , Eout , L0 , N , s0 〉, where: (i) S is a set of state nodes and s0 ∈ S the initial node; (ii) T is a disjoint set of transition nodes; (iii) Ein ⊆ S ×T is a set of input edges; (iv) Eout ⊆ T ×S is a set of output edges; (v) function L0 : T ↦→ Pu represents the user programs labelling transition nodes; and (vi) N ⊆ S∪T is a set of current nodes.

We stipulate that for any node n ∈ S ∪ T there exists a sequence s1 · t1 · . . . · sk-1 · tk-1 · sk, such that s0 = s1, node n is in the sequence, and for each i ∈ [1, k - 1] : (si, ti) ∈ Ein and (ti, si+1) ∈ Eout.

The PRS deliberation cycle consists of three main steps: processing environment updates, e.g., new event-goals or belief updates; instantiating a plan-body graph to achieve an event-goal or goal condition, or executing a single step in an instantiated plan-body graph; and notifying plan-body graphs when conditions they are monitoring are established or violated. Execution of a plan-body graph starts in the initial node (s0), and progresses to one or more state/transition nodes (N). Transition nodes initially represent user programs (L0) and evolve following the semantics in Section 3 until they reach the 'empty program' and terminate. The plan-body graph finishes executing (successfully) if no current state nodes N of G lead anywhere. Formally, the plan-body graph is initial if N = {s0}, and finished, denoted by fin(G), if N ⊆ S, and for all s ∈ N and t ∈ T : (s, t) ̸∈ Ein. All plan-body graphs occurring in a plan-library are initial.

Example 1. Consider an agent that has a goal to travel from its current location to a destination d [Sardina and Padgham, 2011]. The goal can be achieved in various ways depending on the distance to the destination, represented by the following plan-rules (each omitted goal-condition ϕ is ⊤):

travel(d) : At(x) ∧ WalkDist(x, d) ← Gwalk ,

travel(d) : At(x) ∧ ∃y(InCity(x, y) ∧ InCity(d, y)) ← Gcity ,

travel(d) : At(x) ∧ ¬∃y(InCity(x, y) ∧ InCity(d, y)) ← Gfar .

The first plan-rule refers to the plan-body graph Gwalk shown in Fig. 1.

3 PRS Semantics

Our semantics for PRS follows the approach adopted by the CAN [Winikoff et al., 2002] agent programming language, as defined in [Sardina and Padgham, 2011], where a transition relation on agent configurations is defined in terms of a set of derivation rules [Plotkin, 1981]. An agent configuration is a tuple [Π , Λ, B, A, Γ ] where Π is a plan-library, Λ is an actionlibrary, B is a belief base, A is a sequence of executed actions, and Γ is a set of intentions (as Π and Λ do not change during execution, we omit them from derivation rules). Agent configurations represent the execution state of a PRS agent, and intentions are the current states of full programs being pursued in order to achieve top-level event-goals. As in CAN, full programs extend the syntax of user programs to represent the current evolution of a user program, and may contain information used to decide the next transition, e.g. the planbody graphs yet to be tried in achieving an event-goal.

Formally, a full program (or simply program) is a formula in the language defined by the grammar P ::=

where η, ('nil') indicates that there is nothing left to execute; WTx(φ) denotes either WT(φ) or WT(φ), where WT(φ) indicates that program WT(φ) has been adopted (i.e., its execution has started); ev : Lψ1 : G1, . . . , ψn : GnM represents the set of relevant plan-rules for achieving the event-goal or goal-condition ev; P ⇝ P ′ represents a suspended active preserve program P ′ whose associated condition is being re-achieved by a recovery program P; G ▷ P, where P = ev : Lψ1 : G1, . . . , ψn : GnM, represents the default deliberation mechanism for 'goal commitment': achieve ev using an applicable plan-body graph G, but if that fails, try an

Figure 2: PRS derivation rules for actions, belief updates, and goal commitment.

alternative applicable graph from those appearing in P; and η ▷ P indicates that a plan-body graph for ev has succeeded. Note that full programs are more general than those yielded by our semantics.

We first give derivation rules for configurations of the form [Π,Λ, B,A, P], where P is a full program, i.e., for a single intention. We give the derivation rules for actions, belief operations, goal and plan adoption, and goal commitment in Section 3.1; for advancing plan-body graphs in Section 3.2; for PRS-specific wait and preserve programs in Section 3.3; and for agents with configurations of the form [Π , Λ, B, A, Γ ], i.e., multiple intentions, in Section 3.4.

3.1 Semantics for Actions, Belief Updates, Goal and Plan Adoption, and Goal Commitment

Fig. 2 shows the derivation rules for actions and belief operations. Rules add and del simply update B, replacing programs +b and -b with η (A remains unchanged). The semantics for actions is given by rule A. The antecedent checks whether there is a relevant action-rule for act (i.e., one whose 'head' act′ matches act under substitution θ), and whether the action is applicable (i.e., its precondition holds in B); the conclusion of the derivation rule applies the action's add- and delete-lists to B and appends the action to A.

Rule Ev1 adopts the event-goal program !e by creating the set ∆ of plan-rules relevant for the event, i.e, the rules in Π with event-goals matching e via a most general unifier mgu.

Example 2. Processing an event-goal program of the form !travel(Uni) using rule Ev1 yields the following (full) program, encoding all relevant options for this event:

Similarly, rule Ev2 adopts the goal-condition program !φ by creating the set ∆ of plan-rules in Π that can achieve φ.

Rule Sel selects an applicable plan-rule for event-goal or goal-condition ev from the set of relevant rules, and schedules the associated plan-body graph for execution.

Rules for goal commitment are shown in Fig. 2. Rule ▷stp executes a single step in a program G▷ P if the plan-body graph G has neither failed nor finished (see Section 3.2). Rule ▷end discards the alternative program P in a program η ▷ P (where η here represents a completed graph). Finally, rule ▷f schedules the alternative P = ev : L∆M for execution and executes a single step in it, provided G has failed and P has not, i.e., an applicable plan-rule exists for ev.

3.2 Semantics for Plan-Body Graphs

We extend the definition of a plan-body graph in Definition 1 to a full plan-body graph, representing the current 'state' in the evolution of an initial plan-body graph. A full plan-body graph is of the form G = 〈S,T, Ein, Eout , L0 , Lc,N, s0 〉 where Lc : T ↦→ P is a function that maps each transition node t ∈ T to a full program P ∈ P, which represents the current form of the possibly evolved (initial) user program L0(t). We use the following auxiliary definitions: bef (t) = {s | (s, t) ∈ Ein} are the input state nodes of t; aft(t) = {s | (t, s) ∈ Eout} are its output state nodes; and the update to function Lc with a (new) program P for t is

The first rule states that a transition node t, in the case where it is not initially associated with a test condition, becomes active if it is not already active but all of its input states are. Becoming active includes (re-)initialising t to correspond to its user program. This is done in case t is part of a cycle.

Once a transition node t is active, it can perform a single execution step in its associated (current) program Lc(t).

If a transition node's program has finished execution, the node becomes inactive and its outgoing nodes become active.

1 We treat the functions L0 and Lc as relations, i.e., as sets of ordered pairs of the form 〈t , P〉.

Example 3. Suppose that the agent believes it is currently at home, which is walking distance to the university. In this case, the Sel rule transforms the set of relevant options represented by the program in Example 2 into the program Gwalk ▷ travel(Uni) : Lψ2 : Gcity, ψ3 : GfarM, i.e., the agent selects the Gwalk plan-body graph while keeping the other graphs as backup alternatives, represented by the righthand side of the ▷ operator. When the agent starts executing the Gwalk graph, the rule GPstart removes s0 fromN and adds the transition node associated with subgoal !pw. This is then executed using rule GPstp , whose antecedent uses rule Ev1 to resolve the subgoal.

If a transition node is initially associated with a test condition, then the node becomes active only if the condition holds in the current belief base. The chosen transition node also becomes inactive at the same execution step, as once the condition is tested there is nothing left to execute. Under this semantics, PRS allows choices in execution within the graph: either a non-deterministic choice when multiple transition nodes, with non 'mutex' test programs, exit the same state node, or deterministic choices induced by such tests.

The case where B ̸|= φ holds represents failure, i.e., the inability to execute a step in t.

Finally, if a plan-body graph has finished (Section 2), rule Gend replaces it with program η.

Example 4. Consider the evolution Gpw ▷ pw : L∆pwM of subgoal !pw. Achieving the former using the graph in Figure 1 involves the parallel execution of the programs P 1 pw and P 2 pw . This 'split' is represented by the outgoing edges from the transition node associated with the ?⊤ user program, and results in state nodes s4 and s5 being added to N, using rule G?φ stp . Note that for the transition node associated with !ev2 to become active, both P 1 pw and P 2 pw must complete execution, and transition to s6 and s7, respectively.

3.3 Semantics forWait and Preserve Programs

We now give a semantics for wait and preserve programs of the form WT(φ), PRp(P, φ), and PRa(P, φ), and suspended active preserve programs of the form P1 ⇝ PRa(P2, φ), where P1 is the recovery program. In all cases, we assume that condition φ is ground when the program is adopted.

Rule Wadopt adopts a wait program, i.e., changes its form to indicate that condition φ is now being monitored. Rule W specifies that the wait for φ should continue if φ does not hold in the belief base. Finally, rule Wend specifies that the wait should end if φ does hold. In all cases, C = [B, A, WT(φ)].

The first set of derivation rules for preserve programs apply to both passive and active preserves. Rule Pradopt specifies the adoption of a preserve program, i.e., the adoption of its eventgoal or goal-condition program !ev. Rule Prstp executes a single step in a preserve program if φ is not violated, and Prsucc removes a completed preserve program.

Rule Prfail specifies that the passive preserve fails if φ is violated or P is blocked.

Rules APrfail to APrstp2 sus operationalise adopted active and suspended preserve programs. We define three special multisets. 2 Given an expression E that is either a program or planbody graph G = 〈S, T, Ein, Eout, L0, Lc, N, s0〉, we define a 'path' of 'nested' (adopted) preserve and wait programs as any element in the multiset T (E), defined as T (E) =

When E = G we take the multiset union of the sequences corresponding to transition nodes in G that are executed in parallel. The first element in such a sequence is a 'most abstract' preserve or wait program occurring in E, and the last element is a 'most deeply' nested preserve or wait program occurring in E. We use Sτ (E) and Pτ (E) to denote the multisets of all the elements in all the sequences in T (E) that are, and are not, of the form P ⇝ P ′ , respectively; i.e., any element in Sτ (E) is a suspended (adopted) active preserve program, and any element in Pτ (E) is an adopted wait, passive preserve, or active preserve program that is not suspended. We use T (E) to check whether a wait/preserve program in some 'path' in E may be 'pruned' by a more abstract preserve program in the path, and we use Sτ(E) and Pτ(E) to count the number of suspended and unsuspended programs occurring in E.

Example 5. Suppose P 1 pw and P 2 pw have evolved to, respectively, adopted programs WT(φ) and PRp(P, φ′ ), with P = e : L∆M (i.e., one parallel branch waits for a condition φ while the other tries to achieve an event-goal program !e while preserving φ′ ). Then, T (Gwalk) = {WT(φ), PRp(P, φ′ )}. Moreover, if P evolves to P ′ = Ge ▷ e : L∆′ M, where Ge mentions an adopted program, e.g., WT(φ′′ ), then T (Gwalk) = {WT(φ), PRp(P ′ , φ′ ) · WT(φ′′ )}.

2 Adapted from [Sardina and Padgham, 2011].

Figure 3: Agent-level derivation rules; each Ci is an agent configuration, C = [B, A, Γ], and Γ′ = {!e1, . . . , !en}.

Rule APrfail specifies that the adopted active preserve program PRa(P, φ) fails if P fails and the monitored condition φ is not violated. If φ is violated, APrsus suspends the preserve program and attempts to re-establish φ using the recovery (goal-condition) program !φ. Rules APrfail sus and APrunsus specify, respectively, that a suspended preserve program fails if the recovery program fails, and is resumed if the recovery program completes.

Finally, rules APrstp1 sus and APrstp2 sus define the execution of recovery programs and suspended (active preserve) programs. Rule APrstp2 sus executes a single 'cleanup' or 'notification' step in the suspended program. Such an execution step amounts to a program P1 evolving to a program P2 that has fewer suspended programs, or fewer unsuspended preserve or wait programs, e.g. due to a failed passive preserve that had a 'nested' wait program. The relation P ≺ P ′ is defined for programs P and P ′ as: P ≺ P ′ def = |Pτ(P)| < |Pτ (P ′ )| ∨ |Sτ (P )| < |Sτ (P ′ )|.

Note that rule APrstp2 sus implies that if an active preserve is suspended, all of the (possibly adopted) 'nested' programs occurring in P2 are 'implicitly suspended', i.e., they can only perform 'cleanup' or 'notification' steps, so we are guaranteed to terminate.

Proposition 1. Any sequence of configurations [B1 , A1 , P1 ]· . . . · [Bn,An, Pn] is finite if for all i ∈ [1, n - 1], we have that Pi+1 ≺ Pi and [Bi , Ai , Pi ] → [Bi+1 , Ai+1 , Pi+1 ].

Proof. Since each such execution step from Pi to Pi+1 must yield fewer wait programs, preserve programs, and/or programs of the form P ⇝ PRa(P ′ , φ), it is sufficient to consider whether a 'switch' of the latter to resume PRa(P ′ , φ) can lead to it (possibly with an 'evolved' P ′ ) being suspended again, and whether this can continue indefinitely.

For PRa(P ′ , φ) to resume, we must have P = η, and then if φ still does not hold, the program will indeed evolve to !φ ⇝ PRa(P ′ , φ). Moreover, recovery program !φ does have at least one relevant plan-rule, as it was once able to evolve to η (recall that φ has been ground from the moment its associated active preserve program was adopted). However, the only possible execution step on !φ cannot reduce the number of aforementioned programs.

We use the notation C C ′ to denote that there exists a non-empty sequence of configurations from C to C ′ .

3.4 Agent-Level ('Top-Level') Semantics

We now give the derivation rules for the top-level execution of an agent program. Transitions between agent configurations are defined by the derivation rules in Fig. 3; an expression C t =⇒ C′ denotes a transition of type t ∈ {PRS, EVENT, COND, INT}.

Rule Aprs is the top-level rule, and represents the PRS deliberation cycle. A single PRS type execution step comprises three things: progressing an intention by one step, or removing a completed intention (i.e., P = η) or a failed one (using rules Aint or Arem, respectively); processing newly observed event-goals (using rule Aev), i.e., creating an intention for each new event-goal that is observed from the (external) environment; and finally, performing all the necessary 'notification' and 'cleanup' steps on wait, preserve, suspended, and recovery programs (using rule Acond) to leave the agent in a 'sound' or 'stable' configuration. More specifically, Acond takes a single step in an intention if the step will yield an intention with fewer suspended programs, or fewer unsuspended (adopted) preserve or wait programs.

4 Properties of the Semantics

We now prove key properties of the semantics and show the greater expressivity of our PRS fragment compared to CAN. In what follows, we use [B,A, P] → as an abbreviation for ∃B′ ,A′ , P ′ : [B,A, P] → [B′ ,A′ , P ′ ], and C1, C2 are agent configurations of the form [Bi ,Ai , Γi ] such that C1 is sound and C1 PRS =⇒ C2. A configuration C = [Λ,Π, B,A, Γ] is sound iff (i) for all WT(φ) ∈ Pτ(Γ), B ̸|= φ; (ii) for all P ⇝ P ′ ∈ Sτ(Γ), [B,A, P] →; and (iii) for all PRx(P, φ) ∈ Pτ (Γ), B |= φ and [B, A, P] →.

Theorem 1 states that all configurations resulting from applying rule Aprs on a sound configuration are sound.

Theorem 1. Let C1 and C2 be as above. Then, C2 is sound. Proof Sketch. Observe from the antecedent of derivation rule Aprs that only one step of type INT is performed on C1, followed by one of type EVENT, and zero or more of type COND. Assume the theorem does not hold because there is a passive preserve PRp(P, φ) ∈ Pτ(Γ2), for some P, such that B2 ̸|= φ or [B2 ,A2 , P] ̸→. Then, since PRp(P, φ) is an adopted program appearing in some intention PI ∈ Γ2, either rule Prfail or Prsucc can be applied to configuration [B2 , A2 , PRp(P, φ)] to yield an intention P ′ I . Since P ′ I ≺ PI , rule Acond will be applied (possibly multiple times) to PI until PRp(P ′ , φ) ̸∈ Pτ(Γ2) for all P ′ , which contradicts our assumption. Assume instead that the theorem does not hold because there is a program P ⇝ P ′ ∈ Sτ(Γ2) such that [B2 ,A2 , P] ̸→. Then, either rule APrfail sus or APrunsus will be applied to configuration [B2 ,A2 , P ⇝P ′ ] or its 'evolution', again resulting in a contradiction. The remaining cases are proved similarly. □

The next theorem states that an adopted wait program is only removed in a PRS step if either its condition becomes satisfied, or the program is pruned, i.e., it is a descendant of an adopted preserve or a suspended preserve that is discarded. Given a program P and 'path' τ ∈ T (P), we denote the program at index n > 0 as τ[n] (where τ[1] is τ's most abstract program). A program P is pruned between C1 and C2 iff for any τ ∈ T (Γ1) with T (Γ) = ⊎P ′∈Γ T (P ′ ) and τ[k] = P for some k > 0, there exists a 0 < j < k such that: 3

Theorem 2. Let C1 and C2 be as before. For each WT(φ) ∈ Pτ (Γ1) such that WT(φ) ̸∈ Pτ (Γ2), we have that B2 |= φ, or WT(φ) is pruned between C1 and C2.

Proof Sketch. Let WT(φ) ∈ Pτ(Γ1) be a program such that WT(φ) ̸∈ Pτ(Γ2). Let t be a transition node currently labelled with WT(φ), where T = {t, . . .} and N = {t, . . .} are the transition nodes and current nodes in a ('partially executed') plan-body graph G. We consider the case where if B2 ̸|= φ, then WT(φ) must have been pruned between C1 and C2, because no other derivation rules can 'remove' WT(φ). First, rule Gend (which, if applicable, 'removes' G) requires fin(G) to hold, which cannot be the case as t ∈ N; for the same reason, rule GPstart cannot 'reset' WT(φ). Second, the antecedent of rule ▷f requires that [B,A,G] ̸→ (for some A and B ∈ {B1, B2}), which cannot hold as we can take a step on WT(φ) via rule W. Similarly, if P is an intention in which G occurs, the antecedent of agent-level rule Arem cannot hold (i.e., [B1 ,A, P] ̸→ cannot hold for any A). Then, it follows that WT(φ) is pruned between C1 and C2. □

Theorem 3 states that an adopted preserve program is only 'removed' if: its condition becomes violated; its associated program becomes blocked; or the preserve program is pruned.

3 The definitions of Pτ(E) and Sτ(E), for some expression E, can be generalised similarly.

Theorem 3. If C1 and C2 are as before, and PRx(P, φ) ∈ Pτ (Γ1) is a program s.t. PRx(P2, φ) ̸∈ Pτ (Γ2) for any P2:

1. B2 ̸|= φ or [B2 ,A2 , P] [B2 , A2 , P ′ ] ̸→;
2. [B1 ,A1 , P] → [B2 ,A2 , P ′ ] [B3 , A3 , P ′′ ] ̸→; or
3. PRx(P, φ) is pruned between C1 and C2.

Proof Sketch. We show that if two of the conditions above do not hold, then the third will. For example, if (2) and (3) do not hold, then PRx(P, φ) must have been 'removed' by rule Prfail or suspended by APrsus, whose antecedents entail (1). Similarly, if (1) and (2) do not hold, then PRx(P, φ) must have been pruned between C1 and C2 for the reasons given in the proof of Theorem 2. □

Theorem 4 states that a suspended preserve program is only 'removed' during a PRS step if: the recovery program completes and the preserve program's condition is re-established; the recovery program becomes blocked; or both are pruned.

Theorem 4. If C1 and C2 are as before, and P1 ⇝ PRa(P2, φ) ∈ Sτ(Γ1) is a program s.t. P ⇝ PRa(P ′ , φ) ̸∈ Sτ (Γ2) for any P and P ′ :

1. [B1 ,A1 , P1 ] → [B1 ,A1 , η] and B1 |= φ;
2. [B2 ,A2 , P1 ] [B2 , A2 , P ′1 ] ̸→;

1. or P1 ⇝ PRa(P2, φ) is pruned between C1 and C2.

The proof of Theorem 4 is similar to that of Theorem 3.

Theorems 3 and 4 considered the case where all occurrences of preserve programs associated with the same condition φ, e.g. in multiple intentions in Γ1, are removed in a PRS step. There is also the case where only some of them are removed in such a step. It is not difficult to develop theorems for this case, though we would need additional formal machinery. Similarly, we can show that active preserve programs are suspended and resumed for the right reasons. For example, with a minor extension to Theorem 3, we can show that if PRa(P, φ) becomes suspended (i.e., !φ ⇝ PRa(P, φ) ∈ Sτ (Γ2)), then B2 ̸|= φ and [B2 , A2 , !φ] → hold.

In the remainder of this section, we characterise the relative expressivity of our PRS fragment and the CAN formalism as defined in [Sardina and Padgham, 2011]. A CAN plan-rule is of the form e : ψ ←P, where e is an event-goal, ψ is a context condition, and P is a plan-body, i.e., a formula in the language defined by the grammar P ::=

where P1; P2 is sequential composition, P1 ‖ P2 is parallel composition, and Goal(φs, P ′ , φf) is a declarative goal specifying that formula φs (the goal) should be achieved using program P ′ , failing if φf becomes true. The remaining programs are defined as for PRS user programs.

To state our results, we need the notions of execution traces and solutions. We define these only for PRS as the definitions for CAN are analogous.

Definition 2. An execution trace of an agent configuration C = [Λ,Π, B,A, Γ] is a finite sequence of agent configurations C1 · . . . · Cn such that C = C1 and Ci PRS =⇒Ci+1 for all i ∈ [1, n - 1]; the solution in C1 · . . . · Cn is the sequence A of actions such that An = A1 · A.

With Λ, Π, B, and Γ as above, SOL(Λ, Π, B, Γ) denotes the set of solutions, i.e., the set of sequences of actions performed in the execution traces of configuration [Λ, Π , B, ϵ, Γ ], where ϵ denotes the empty string. Theorem 5 states that a CAN plan-library Π-c not mentioning Goal(φs, P, φf) programs (as there is no corresponding program in PRS) can be translated into an equivalent PRS plan-library.

Theorem 5. If Π-c is a CAN library and Λ an action-library, there exists a PRS library Πp s.t. for any event-goal !e and beliefs B: SOL(Λ,Π-c , B, {!e}) = SOL(Λ,Πp, B, {!e}).

Proof Sketch. Given a CAN plan-rule e : ψ ←P ∈ Π-c , the first step is to obtain the corresponding PRS planrule e : ⊤; ψ ←G. We define three functions: g(P, n)in, g(P, n)out, and g(P, n)L, where n ∈ N. When n = 1, these functions represent respectively the elements Ein, Eout, and L0 in G. If P = act, we define g(P, n)in = {(n · s, n · t)}; g(P, n)out = {(n · t, n · s′ )}; and g(P, n)L = {〈n · t, P〉}, where s, s′ and t are unique symbols (and thus, n · t, for example, is a string). We also define g(P, n)start = n · s and g(P, n)end = n · s′ . Intuitively, n uniquely identifies the PRS plan-body 'subgraph' corresponding to P. If P = P1; P2 is the sequential composition of CAN programs P1 and P2,

where transition node n · t′ 'connects' the subgraphs corresponding to P1 and P2. As before, we define g(P, n)start = n · s and g(P, n)end = n · s′′ , and s, s′′ , t, t′ and t′′ are unique symbols. We similarly define the subgraph corresponding to a CAN parallel composition P1||P2, test program, etc.

We then show by induction on the structures of P and G above that their traces yield the same solutions. For example, the derivation rules for CAN's sequential composition can be simulated by repeatedly applying the GPstart ,GPstp and GPend rules of PRS, and vice versa. □

Theorem 6 states that the converse does not hold: even if we ignore programs that have no counterparts in CAN, PRS plan-libraries cannot be 'directly mapped' to CAN libraries. This result follows from a similar one in [de Silva, 2017] which showed that the 'plan-body' representation used in HTN planning allows a more fine-grained interleaving of steps than do CAN plan-bodies: a CAN plan-body must specify steps in a 'series-parallel' manner, whereas HTN 'planbodies' (and PRS plan-body graphs) do not.

In what follows, Π-p denotes PRS plan-libraries that do not mention goal-condition, wait, nor preserve programs, and Πc ∈ CAN(Π-p ) denotes a directly mapped CAN library, i.e., one obtained from Π-p by ignoring the goal-condition ϕ in each plan-rule, and replacing each graph G appearing in Π-p with a CAN plan-body P such that the multisets of (user) programs occurring in G and P are the same.

Theorem 6. There exists a PRS library Π-p , an action-library Λ, and event-goal !e, s.t. for any CAN library Πc ∈ CAN(Π-p ) and beliefs B: SOL(Λ, Π-p , B, {!e}) ̸= SOL(Λ, Πc, B, {!e}). Proof Sketch. We translate an example HTN 'plan-body' provided in [de Silva, 2017] into a PRS plan-body graph. First, we create the PRS plan-rule etop : ⊤;⊤←G, in particular

by taking the following input and output edges for G:

Second, we set the initial program L0(ti) for each ti ∈ {t1, . . . , t6} to a different event-goal eti , each of which is associated with a single plan-body graph representing the sequence of unique actions a1ti · a2ti . Finally, we show that the following sequence of actions:

cannot be produced by any CAN trace of program !etop, relative to any CAN plan-library that is directly mapped from the above set of PRS plan-rules; e.g., the CAN body et1 ; (et2 ‖ (et3 ; et5 )); et4 ; et6 does not allow a2t5 to follow a2t4 . □

5 Discussion

We proposed an operational semantics for a significant fragment of the OpenPRS variant of PRS that accounts for (possibly nested) graph-based plan-bodies; language features such as active preserves; and for adopting, suspending, resuming, and aborting such programs. We showed that our semantics is sound, correctly accounts for the key interactions between (nested) wait and preserve programs, and that planbody graphs do not have a direct translation to plan-bodies in a typical BDI-based agent programming language (CAN).

Our work is closely related to that of Dastani et al. [2011] on the semantics of resuming, suspending, and aborting maintenance goals. They define complex goal types that include achievement of goal formulas, maintenance goals and complex temporal goals. All of these can be encoded as planbody graphs in PRS through a straightforward mapping. Van Riemsdijk et al. [2009] develop a modal logic for goal representation and reasoning mechanisms for non-temporal goals. While the goal types they consider could probably be represented as PRS plan-body graphs, encoding the associated mechanisms for reasoning about goal conflicts is less straightforward. Thangarajah et al. [2011; 2014] define an operational semantics for various types of goals, most of which can be implemented using PRS plan-body graphs and programs. However, their maintenance goals include a construct to proactively maintain a goal condition by anticipating whether it will fail. This specific capability of predicting conditions in the future is lacking in our semantics.

Future work includes investigating whether an arbitrary PRS plan-rule can be simulated by a set of CAN (or AgentSpeak) plan-rules, and extending our semantics to add more PRS features, e.g. meta-level reasoning and plan steps that can overlap in execution.

Acknowledgements

Lavindra is grateful to F´elix Ingrand for useful discussions about OpenPRS while Lavindra was a researcher on the GOAC/MARAE projects (2009-2011) at LAAS-CNRS. Felipe thanks CNPq for partial financial support under its PQ fellowship, grant number 305969/2016-1.