Composition of ConGolog Programs

1 Introduction

In this paper, we study the composition of possibly nonterminating high-level programs over action theories. We assume:

• an action theory, expressed in the situation calculus [Reiter, 2001], describing how actions affect the state of affairs of the domain of interest;
• a library of available high-level programs over such action theory, expressed in (a significant fragment of) ConGolog [De Giacomo et al., 2000], and which may stand for behavioral descriptions of actual devices (e.g., a controller for an elevator or a coffee delivery robot), the capabilities or logic of some services (e.g., a webservice), or even descriptions of typical operational procedures in the domain (e.g., a business process); and
• a target program over the same action theory that is not in the library, expressed again in ConGolog, which may stand for a behavior of interest that does not directly correspond to any of the available modules.

The problemwe investigate is as follows: verify whether, for a given initial configuration of the world, expressed as a possibly infinite database (i.e., a categorical theory), the target

Giuseppe De Giacomo

Dipartimento di Informatica e Sistemistica Sapienza Universit`a di Roma Roma, Italy

degiacomo@dis.uniroma1.it

program executions can be "realized" by composing fragments of the executions of the available programs so as to mimic the (virtual) transitions (i.e., elementary steps) of the target program at each point in time. If so, synthesize a delegator that does the composition automatically.

This kind of composition problem has been investigated first in the CS literature, e.g., [Berardi et al., 2003; Traverso and Pistore, 2004; Lustig and Vardi, 2009], 1 and then also in AI, e.g., [De Giacomo and Sardina, 2007; Sardina et al., 2008], but always assuming finite state settings. 2 Here, instead, we investigate the problem in a setting that allows us to consider potentially infinite domains that may go through an infinite number of states as actions are performed.

Specifically, we formally define what it means for a set of ConGolog programs to mimic the transitions of a target program, by using a greatest fixpoint second-order formula based on a suitable adaptation for our context of the formal notion of Simulation [Milner, 1971; Sardina et al., 2008].

Obviously, in checking such fixpoint formula over ConGolog programs is undecidable in general. Nonetheless, by exploiting recent ideas in the AI literature [Pirri and Reiter, 1999; Kelly and Pearce, 2007; Claßen and Lakemeyer, 2008], we are able to devise a sound and well characterized procedure to solve the problem. The technique is based on three basic ingredients: (i) computation of the simulation through fixpoint approximates [Tarski, 1955], hoping to be able to compute the fixpoint in a finite number of iterations; (ii) use of the characteristic graphs introduced by Claßen and Lakemeyer [2008], to finitely cope with the potential infinite branching of ConGolog programs (due to ConGolog's πx.δ construct); and (iii) use of regression [Reiter, 2001] to get formulas that talk only about the initial situation, thus allowing us to drop the action theory and the second-order foundational axioms for situations altogether.

1 Notice that ConGolog has already been considered in the context of web-service composition in [McIlraith and Son, 2002], by exploiting procedural abstraction. But the form of composition studied there is profoundly different from the one considered here.

2 A notable exception is [Berardi et al., 2005], where programs were executed over a database which may go through an infinite set of configuration. However, the techniques proposed there were again based on being able, under suitable assumptions, to reduce the setting to a finite state one.

2 Preliminaries

The situation calculus is a logical language specifically designed for representing and reasoning about dynamically changing worlds [Reiter, 2001]. All changes to the world are the result of actions, which are terms in the language. We denote action variables by lower case letters a, action names by capital letters A, and non-variable action terms by α, possibly with subscripts. A possible world history is represented by a term called a situation. The constant S0 is used to denote the initial situation where no actions have yet been performed. 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. Relations whose truth values vary from situation to situation are called fluents, and are denoted by predicate symbols taking a situation term as their last argument (e.g., Holding(x, s)).

Within the language, one can formulate action theories that describe how the world changes as the result of the available actions. Here, we concentrate on basic action theories [Pirri and Reiter, 1999; Reiter, 2001]. A basic action theory D is the union of the following disjoint sets: the foundational, domain independent, axioms of the situation calculus (Σ); precondition axioms stating when actions can be legally performed (Dposs); successor state axioms describing how fluents change between situations (Dssa); unique name axioms for actions (Duna); and axioms describing the initial configuration of the world (DS0 ). A special predicate Poss(a, s) is used to state that action a is executable in situation s; precondition axioms in Dposs characterize such predicate. In turn, successor state axioms encode the causal laws of the world being modelled; they take the place of the so-called effect axioms, but can also provide a solution to the frame problem. For example, in a music matchbox setting, a song is pending to be played if the it has just been requested, via the matchbox interface, and it is available in some CD, or the song was already pending for playback and the matchbox has not just started playing it: 3

Pending(song, do(a, s)) ≡ (a = requestSong(song) ∧ (∃cd)InDisk(song, cd)) ∨ P ending(song, s) ∧ a ̸= playBack(song).

Once the dynamical system is modeled as a basic action theory, one can pose queries about its behavior or evolution as logical entailment queries relative to the theory.

High-Level Programs. 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, such as Golog [Levesque et al., 1997], which includes usual structured constructs and constructs for nondeterministic choices, ConGolog [De Giacomo et al., 2000], which extends Golog to accommodate concurrency, and IndiGolog [Sardina et al., 2004], which provides means for interleaving planning and execution.

Here we concentrate on a fragment of ConGolog, which includes most constructs of the language, with the notable exception of (recursive) procedures:

3 Here, we implicitly quantify all free variables universally.

α atomic action φ? test for a condition δ1; δ2 sequence δ1|δ2 nondeterministic branch πx.δ nondeterministic choice of argument δ∗ nondeterministic iteration if φ then δ1 else δ2 endIf conditional while φ do δ endWhile while loop δ1‖δ2 concurrency

Above, α is an action term, possibly with parameters, and φ is situation-suppressed formula, that is, a formula in the language with all situation arguments in fluents suppressed. We denote by φ[s] the situation calculus formula obtained from φ by restoring the situation argument s into all fluents in φ.

Note the presence of nondeterministic constructs, which allow the loose specification of programs by leaving "gaps" that ought to be resolved by the executor. 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 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.

As an example, consider the nondeterministic controller δmatchbox for a music matchbox that serves users' requests:

while True do if (¬Playing ∧ (∃song)Pending(song)) then (πsong, disk) (P ending(song) ∧ InDisk(song, disk))?; selectSong(song); loadDisk(disk); playBack(song) else wait endWhile

That is, when the matchbox is idle and there is a song pending to be played, the controller selects a song that has been requested and the CD in which the song is, loads such CD, and starts the playback. When the matchbox is playing a song or there are no pending songs to be played, the device just waits. A full music system is modeled by taking program δmusic = (δmatchbox‖ δEXO), where δEXO = (πa.Exog(a)?; a)∗ represents the (external) environment, capable of executing any exogenous action (e.g., requestSong(song)) at anytime.

Formally, the semantics of ConGolog is specified in terms of single-steps, using the following two predicates [De Giacomo et al., 2000]: (i) Final(δ, s), which holds if program δ may legally terminate in situation s; and (ii) Trans(δ, s, δ′ , s′ ), which holds if one step of program δ in situation s may lead to situation s′ with δ′ remaining to be executed. The definitions of Trans and Final for the constructs used in this paper are shown below:

Final(α, s) ≡ False Final(φ?, s) ≡ φ[s] Final(δ1; δ2, s) ≡ Final(δ1, s) ∧ Final(δ2, s) Final(δ1|δ2, s) ≡ Final(δ1, s) ∨ Final(δ2, s) Final(πx.δ, s) ≡ ∃x.F inal(δ, s) Final(δ∗ , s) ≡ True Final(δ1‖δ2, s) ≡ Final(δ1, s) ∧ Final(δ2, s)

Trans(α, s, δ′ , s′ ) ≡ s′ = do(α, s) ∧ Poss(α, s) ∧ δ′ = True? Trans(φ?, s, δ′ , s′ ) ≡ False Trans(δ1; δ2, s, δ′ , s′ ) ≡ Trans(δ1, s, δ′1 , s′ ) ∧ δ′ = δ′1 ; δ2 ∨ Final(δ1, s) ∧ Trans(δ2, s, δ′ , s′ ) Trans(δ1|δ2, s, δ′ , s′ ) ≡ T rans(δ1, s, δ′ , s′ ) ∨ T rans(δ2, s, δ′ , s′ ) Trans(πx.δ, s, δ′ , s′ ) ≡ ∃x.T rans(δ, s, δ′ , s′ ) Trans(δ∗ , s, δ′ , s′ ) ≡ Trans(δ, s, δ′′ , s′ ) ∧ δ′ = δ′′ ; δ∗ Trans(δ1‖δ2, s, δ′ , s′ ) ≡ Trans(δ1, s, δ′1 , s′ ) ∧ δ′ = δ′1 ‖δ2 ∨ Trans(δ2, s, δ′2 , s′ ) ∧ δ′ = δ1‖δ′2

Following [Claßen and Lakemeyer, 2008], and differently form [De Giacomo et al., 2000], the test construct φ? here does not yield any transition, but it is final when satisfied. In other words, it is a synchronous version of the original test construct (it does not allow interleaving). With this choice, the ConGolog constructs for conditional and while-loop, which are based on synchronous tests, are immediately definable in terms of the other constructs: if φ then δ1 else δ2 endIf = φ?; δ1|¬φ?; δ2 and while φ do δ endWhile = (φ?; δ)∗ ; ¬φ?.

Also, in this paper, we shall require that in programs of the form πx.δ, the variable x occurs in some non-variable action term in δ, disallowing the occurrence of x only in tests and as an action itself. In this way, πx.δ acts as a construct for the nondeterministic choices of action parameters. Finally, we assume wlog that each occurrence of the construct πx.δ in a program uses a unique fresh variable x-no two occurrences of such a construct use the same variable.

Observe that, since we are not considering recursive procedures here, we do not need to resort to a second-order definition of Trans and Final, though we still need to consider programs as terms, cf. [De Giacomo et al., 2000].

From now on, we will denote by Axioms the situation calculus action theory D that formalizes the domain of interest plus the axioms for Trans and Final.

3 ConGolog Composition

The problem we are interested in is the following. Given a basic action theory, available programs δ0 1 , . . . , δ0n , and a target ConGolog program δ0 t , we want to "execute" δ0 t by concurrently executing δ0 1 , . . . , δ0n , while controlling their interleaving in a suitable way. In other words, we provide to the client the ability of writing virtual target programs over a specific domain of interest, but instead of executing such target programs directly, we actually execute programs from a library of available programs in a way that mimics the target.

As an example, consider the target program δt = [(a; b|d; c); h]∗ in an environment where, for simplicity, all actions are always possible. Such program is virtual, and assume all we can do is to execute concurrently two available programs at hand, namely, δ1 = (a; h | c | a; b)∗ and δ2 = (b | d; h)∗ . It is not difficult to see that, by intelligently scheduling δ1 and δ2, one can realize any execution of δt. For instance, if δt starts by requesting the execution of action a, then one should execute δ1 one step by selecting its first nondeterministic program (a; h); after that δt may only request action b followed by h, which can be realized by advancing programs δ2 first and δ1 then; finally, δt may next either stop, in which case both δ1 and δ2 can be legally stopped as well, or start again, in which case the two available programs can be restarted. An analogous argument applies when δt happens to request action d initially. What is important to note here is that we do not assume to have control on the way that δt may (virtually) execute, while we do have control on the way the available programs are executed. In other words, we have no control on the interpreter executing δt and δt's nondeterminism is therefore "devilish," while we have total control on the interpreter executing the concurrent program δ1‖ . . . ‖δn, whose nondeterminism is "angelic."

To side-step the issue of offline vs. online execution of programs (cf. Conclusion), we assume here to have complete information on the initial situation, that is, Ds0 is indeed a possibly infinite database. Observe that while this is obviously a simplification it does not help wrt the main difficulty of this setting: programs can be legally nonterminating (they describe processes), and the number of configurations (pairs program-situation) a program goes through is potentially infinite. Indeed, the number of states the domain of interest goes through as actions are performed are infinite and unrestricted, if not by the action theory. Also, the states of the programs can be infinite due to the presence of the πx.δ construct, which introduces unbounded branching-there are potentially infinitely many possible remaining programs after program πx.a(x); δ(x) executes its first action a(x), namely, δ(t) for each possible term t in the domain. This implies that the techniques coming from model checking-based verification and synthesis that have emerged as effective lately, and been used for instance in [Sardina et al., 2008], cannot be applied.

To formally define what it means for a program to "mimic" another one, we rely on the formal notion of simulation [Milner, 1971; Sardina et al., 2008]. In our setting, such a notion can be captured by a second-order formula that makes use of Trans and Final. Specifically, we define the predicate Sim(δt, δ1, . . . , δn, s) as the largest predicate S satisfying the condition Θ[S](δt, δ1, . . . , δn, s):

where Θ[S](δt, δ1, . . . , δn, s) stands for the following formula:

By Knaster&Tarski Theorem [Tarski, 1955], the predicate Sim has the following notable properties:

Proposition 1. Sim satisfies the condition Θ, that is,

is valid. Moreover, every predicate S satisfying the condition Θ is "smaller" than Sim, that is, the following is valid:

Intuitively, the formula Sim(δt, δ1, . . . , δn, s) says that (i) if the target program δt may legally terminate in s, so can all the available programs δ1, . . . , δn; and that (ii) whatever transition the target program δt may make in the current situation s, such a transition can be "mimicked" by one of the available programs δi while the other programs remain still, and at the next step the same is true again, and again forever.

Once we have defined Sim, it is easy to write a formula that actually returns the "mimicking" transition:

SimTransi(δt, δ1, . . . , δn, s, δ′t , s′ , δ′i ) says that a target transition from (δt, s) to (δ′t , s′ ) can be mimicked by legally advancing the i-th available program to δ′i . By the definitions of Sim and SimTrans we get:

Proposition 2. The following formula is valid:

Hence, if Sim(δt, δ1, . . . , δn, s) is currently true, then we can use the formulas SimTransi to choose how to mimic the target transitions now, knowing that, in the future, we will be able to continue mimicking the target. This is the base of an interpreter that executes the target program by actually delegating the target transitions to the available programs, thus realizing the composition. The interpreter, or delegator, is shown in Procedure 1.

Procedure 1 DELEGATOR(δt, δ1, . . . , δn)

1: if ¬Sim(δt, δ1, . . . , δn, S0) then 2: fail 3: end if 4: loop 5: if Final(δt, s) then 6: Ask whether to stop 7: if stop then 8: exit 9: end if 10: end if 11: Ask δ′t , s′ s.t. Trans(δt, s, δ′t , s′ ) 12: Choose i, δi s.t. SimTransi(δt, δ1, . . . , δn, s, δ′t , s′ , δ′i ) 13: Execute the transition from (δi, s) to (δ′i , s′ ) 14: δt := δ′t ; s = s′ ; δi := δ′i 15: end loop

Observe that the choices at line 12 are guaranteed to be possible being Sim(δt, δ1, . . . , δn, S0) true. Also, observe that, with the assumption of complete information on the initial situation, all checks on formulas consist in formula evaluation, though over a possibly infinite model (cf. Conclusion).

4 The Technique

It remains to find means to check for Sim(δt, δ1, . . . , δn, s). Notice that this is a hard problem in general even if we have complete information on the initial database. The difficulty is that the interpretation structure to be considered is in general infinite, while direct algorithms to check for simulation work only for finite cases.

In order to tackle the infinite case, we follow an approach inspired by [Pirri and Reiter, 1999; Kelly and Pearce, 2007; Claßen and Lakemeyer, 2008]: reduce the verification of a second-order formula wrt the whole basic action theory, to the verification of a first-order formula that is uniform in the situation argument, which, in turn, can be regressed to a formula that only talks about the initial situation.

In particular, we devise a procedure that extracts a firstorder formula that is true on the initial database iff the target program can be simulated by the available programs. Since such a procedure reduces checking a second-order formula to checking a first-order one, it may not terminate in general.

The procedure is based on three ingredients, namely, fixpoint approximates, regression, and programs' characteristic graphs. We detail each of these ingredients below.

Sim approximates. Approximates Simk(δt, δ1, . . . , δn, s), for k ≥ 0 say that program δt may be simulated by programs δ1, . . . , δn in situation s for k steps. Such approximates can be formally defined by induction as follows:

Sim0(δt, δ1, . . . , δn, s) ≡ (Final(δt, s) → ∧ni=1 Final(δi, s)). Simk+1(δt, δ1, . . . , δn, s) ≡ Simk(δt, δ1, . . . , δn, s) ∧ (∀δ′t , s′ .Trans(δt, s, δ′t , s′ ) → ∨ni=1 [∃δ′i .Trans(δi, s, δ′i , s′ ) ∧ Simk(δ′t , δ1, . . . , δi-1, δ′i , δi+1, . . . , δn, s′ )]).

Informally, Sim0 merely requires that whenever program δt is final, so are all programs δ1, . . . , δn; while Simk+1 requires that δt is in k-simulation with δ1, . . . , δn and that every transition of δt can be mimicked by some available program δi and be in k-simulation in the resulting next step.

By Knaster&Tarski classical result on fixpoints approximates [Tarski, 1955], we get:

Proposition 3. If there exists a k ≥ 0 such that

then

We observe that while there is no guarantee that a finite k exists for the antecedent of this proposition to hold, if it does exist, then one can use approximates to compute Sim.

Regression. One of themost important features of basic action theories is the existence of a sound and complete regression mechanism for answering queries about situations resulting from performing a sequence of actions [Pirri and Reiter, 1999; Reiter, 2001]. In a nutshell, the so-called regression operator R∗ reduces a formula φ about some future situation to an equivalent formula R∗ [φ] about the initial situation S0, by basically substituting fluent relations with the right-hand side formula of their successor state axioms.

In this paper, we shall use a simple one-step only variant R of the standard regression operator R∗ for basic action theories. Let φ be a situation-suppressed formula and α be a non-variable action term. Then R[φ[do(α, s)]] stands for the one-step regression of φ through action α, which is in itself a formula uniform in s. It is straightforward to adapt Pirri and Reiter [1999]'s regression theorem to get the following result:

Theorem 4. Let D be a basic action theory, φ a situationsuppressed formula, and α a non-variable action term. Then,

Furthermore, if α1, . . . , αn are ground non-variable action terms, then

That is, operator R reduces a formula about situation do(α, s) to a formula about situation s. By several applications of R, hence, one can reduce formulas about future situations of S0 to formulas about the initial situation only, which can then be verified/answered by first-order entailment/evaluation using only the initial database DS0 and Duna, a much simpler task.

Characteristic graphs. In order to compactly represent all possible configurations a program δ0 may be in during its execution, we shall use the so-called characteristic graph Gδ0 of δ0 introduced by Claßen and Lakemeyer [2008]. The nodes V in a characteristic graph Gδ0 are tuples of the form 〈δ, χ〉, stating that δ is a possible remaining program during δ0 's execution and χ characterizes the conditions under which δ may terminate (i.e., it is final). The initial node is v0 = 〈δ0 , χ0 〉. Edges in Gδ0 stand for single transitions between program configurations and are labeled with tuples of the form 〈π⃗x : α, ψt〉, where α is a non-variable action term and variables ⃗x may appear free in α and ψt. Roughly speaking, an edge states that a program may evolve into another remaining program when one chooses instantiations for ⃗x and performs action α in a situation where ψt holds.

Figure 1 depicts the characteristic graph for the music system example of Section 2. The edge from v0 to v1, for instance, represents those transitions in which a requested song is selected for playback. For that to happen, the program requires to pick a song and a compact disk such that the song is currently being requested, it is in the chosen disk, and the matchbox is currently not playing. Under such circumstances, the program may select the song in question, provided the precondition of such action holds, and evolve to node v1. The program may next evolve to node v2 by loading the chosen disk, provided the precondition of the loading action is true. When program is node v0, it executes action wait whenever there is no song requested for playback or the matchbox is currently playing a song. Finally, we observe that in each node, the system program may execute an exogenous actions (e.g., requestSong(song)) and stay in the same node, that is, in the same program configuration.

v0 = 〈δmusic‖ δEXO, False〉

v1 = 〈(loadDisk(disk); playBack(song))‖ δEXO, False〉

v2 = 〈playBack(song)‖ δEXO, False〉

Figure 1: Characteristic graph for program δmusic.

Next propositions can be shown by induction on the program structure under the assumption that the variable x from each construct πx.δ used in δ occurs in an action term of δ.

Proposition 5. Given a node (δ, χ), we have that

Axioms |= ψ[s] ∧ Poss(α, s) ≡ Trans(δ, s, δ′ , do(α, s)).

5 The Procedure

Given the target program δ0 t and the available programs δ0 1 , . . . , δ0n (wlog we assume that such programs do not share variables) we compute a relation whose tuples have the form 〈vt, v1, . . . , vn, ϕ〉 where vt, v1, . . . , vn are nodes in the characteristic graphs Gδ0 t ,Gδ0 1 ,. . . ,Gδ0n respectively, and ϕ is a firstorder formula. Such tuples intuitively mean that the target program in vt is simulated by the available programs in 〈v1, . . . , vn〉 "iff ϕ holds".

Procedure 2 SYMSIM(δ0 t , δ0 1 , . . . , δ0n ) Compute characteristic graphs Gδ0 t ,Gδ0 1 ,. . . ,Gδ0n X := {〈(δt, χt), (δ1, χ1), . . . , (δn, χn), χt → ∧ni=1 χi〉 | (δj, χj) in Gδ0 j , j ∈ {t, 1, . . . , n}} Xold := ∅ while X ̸= Xold do Xold := X X := NEXT[X] end while return X

Specifically we compute such a relation through the fixpoint procedure in Procedure 2, where the operator NEXT[X] represents a "one step refinement" of the simulation: it updates the formulas ϕ in the tuples 〈vt, v1, . . . , vn, ϕ〉 through one step of regression while maintaining the simulation Sim. In other words, X represents the approximates of the simulation, which are refined at each iteration of the procedure. Formally:

where ϕnew stands for the following formula:

As usual, we assume that ∧ involving zero conjuncts is equal to True and ∨ involving zero disjuncts is equal to False. Note that in each iteration there will be at most one tuple 〈vt, v1, . . . , vn, ϕ〉 ∈ X for each 〈vt, v1, . . . , vn〉. Note also that as soon as we recognize ϕ ≡ false in a tuple 〈vt, v1, . . . , vn, ϕ〉 ∈ X we can stop processing it.

We are now ready to state our core result:

Theorem 7. Let δ0 t , δ0 1 , . . . , δ0n be ConGolog programs, and assume that the procedure SYMSIM(δ0 t , δ0 1 , . . . , δ0n ) terminates returning the set X. Then,

Proof (Sketch). We show by induction on ℓ, and exploiting Proposition 5 and 6, that in the ℓ-th while iteration performed by procedure SYMSIM, the following holds:

By considering Theorem 7 together with the soundness and completeness of regression (cf. Theorem 4) we get:

Theorem 8. Let δ0 t , δ0 1 , . . . , δ0n be ConGolog programs. Assume that the procedure SYMSIM(δ0 t , δ0 1 , . . . , δ0n ) terminates returning the set X. Then, for every ground situation term S:

Based on these results, we can define a version of the delegator in Procedure 1 that works by evaluating first-order formulas only, as shown in Procedure 3. Roughly speaking the new delegator maintains, throughout the execution, the current node (in their corresponding characteristic graph) of each available program (δi, χi) and the target (δt, χt), together with their current bindings θi and θt, respectively. At every iteration, the delegator first checks whether the target program may be entitled for termination, by checking the formula in the current target node (line 11). Notice that if this is the case, then the available programs are also entitled for termination, since Sim holds. If termination is not an option or is not requested, then the next step is asked to the target module. This

Procedure 3 FOLDELEGATOR(δt, δ1, . . . , δn)

1: Compute X = SYMSIM(δ0 t , δ0 1 , . . . , δ0n ) 2: Let 〈(δ0 t , χ0t ), (δ0 1 , χ01 ), . . . , (δ0n , χ0n ), ϕ0 〉 ∈ X 3: if DS0 ∪DUNA ̸|= ϕ0 [S0] then 4: fail 5: end if 6: for all i ∈ {t, 1, . . . , n} do 7: δi:= δ0 i ; χi:= χ0i ; θt:= ∅ // initialization 8: end for 9: S:= S0; // init current situation 10: loop 11: if DS0 ∪DUNA |=R∗ [χtθt[S]] then 12: Ask whether to stop // target may stop 13: if stop then 14: exit 15: end if 16: end if

• 18: Choose i, δ′i , θ′i s.t. (a) (δi, χi) π⃗y αi/ψi -→ (δ′i , χ′i ) ∈ Ei; (b) 〈(δ′t , χ′t ), (δ1, χ1), . . . , (δ′i , χ′i ) . . . , (δn, χn), ϕ〉 ∈ X; (c) αtθtθ′t = αiθiθ′i ; (d) DS0 ∪ DUNA |= R∗ [ψiθiθ′i [S]]; and (e) DS0 ∪ DUNA |= R∗ [ϕ[do(αtθtθ′t , S)]]
• 19: Execute transition fromconfiguration (δiθi, S) to configuration (δ′i θiθ′i , do(αtθtθ′t , S))
• 20: S := do(αtθtθ′t , S) // new current situation
• 21: δt := δ′t ; χt := χ′t ; θt:=θtθ′t ; // update target
• 22: δi := δ′i ; χi := χ′i ; θi:=θiθ′i ; // update program i
• 23: end loop

amounts to asking for a transition in the target graph, and an action αt and a binding θ′t (line 17). In step 18, the delegator finds an available program δi such that its current node can legally transition to a new node by matching the action αt that has been requested and guaranteeing the simulation (we know there is at least one such i, since Sim holds). Finally, the selected program is executed one step accordingly (line 19), the current situation is updated to include the just satisfied action αt, and the current nodes and bindings for the target and program i are updated (line 21-22).

As a direct consequence of Theorems 5, 6, 7, and 4, we obtain:

Theorem 9. If SYMSIM(δ0 t , δ0 1 , . . . , δ0n ) terminates, then FOLDELEGATOR(δt, δ1, . . . , δn) is a sound and complete implementation of DELEGATOR(δt, δ1, . . . , δn).

In other words, for every initial database, FOLDELEGATOR will produce exactly the same input/output behavior, at each point in time, of procedure DELEGATOR.

6 Conclusion

In this paper, we looked at the problem of composing a desired high-level program by suitably executing concurrently a set of available programs at hand. Our technique is able to handle programs that may not terminate and that run over domains that may go through an infinite number of states. We observe here that if the initial database is finite, then the delegator in Procedure 3, which only requires to evaluate firstorder formulas, can be readily implemented using standard relational database technology.

As mentioned, having complete information on the initial situation at runtime allowed us to side-step the issue of offline vs. online executions of high-level programs [Sardina et al., 2004]. Indeed, under complete information of the initial situation the two kinds of execution styles coincide. To extend our approach to deal with incomplete information on the initial situation, more work has to be done. In particular, while the delegators in Procedure 1 and Procedure 3 remain formally well-defined (using entailment instead of formula evaluation), they may not be able to carry out the composition, as they may get stuck by not being able to decide the truth value of a formula. This is a subtle issue, which has been investigated in the context of epistemic feasibility of plans, see e.g., in [Sardina et al., 2004], and which becomes crucial also in our composition context.

The main limitation of the approach proposed here is the lack of (sufficient) conditions guaranteeing termination of procedure SYMSIM. Indeed, finding cases for which we have guarantees of termination of a procedure that eliminates fixpoints (as in this paper, or [Claßen and Lakemeyer, 2008] and [Kelly and Pearce, 2007]) is an interesting research direction for future work.

Acknowledgments

We thank the reviewers for their interesting comments. Sebastian Sardina was supported by Agent Oriented Software and the Australian Research Council (under grant LP0882234), and the National Science and Engineering Research Council of Canada (under a PDF fellowship).