Introduction

Service composition, a well-established topic in the field of Web services, refers to the ability to combine Web services into a business process. More properly, it involves managing and sequencing interactions between Web services, orchestrating them into a larger transaction. This approach enhances the flexibility and adaptability of business processes by enabling them to be constructed from reusable services, allowing organizations to quickly adjust their processes in response to changing business requirements or technological advancements. For example, a transaction involving the addition of a customer to a bank account service could concurrently initiate the creation of multiple accounts while updating the customer information within the customer service. All of these requests are managed in the context of a larger business process flow that either succeeds or fails as a whole [1]. The problem of service composition has been considered in the literature for over two decades. Particularly interesting in this context is the so-called Roman Model [2,3,4] where services are conversational, i.e., have an internal state and are procedurally described as finite transition systems (TS), where at each state the service offers a certain set of actions, and each action changes the state of the service in some way. The designer is interested in generating a new service, called target, which is described as the other service; however, it is virtual in the sense that no code is associated with its actions. Therefore, to execute the target, one has to delegate each of its actions to some of the available services by suitably orchestrating them, taking into consideration the state of the target and the available services are in. Service composition amounts to synthesizing a controller that can suitably orchestrate the executions of the available services so as to guarantee that the target actions are always delegated to some service that can actually execute them in its current state. The original paper on the Roman Model [2] has been the inspiration for a line of work in AI on behaviour composition where nondeterminism, in the sense of partial controllability as in Fully-Observable Non-Deterministic (FOND) strong planning [5,6]) has played a prominent role [7]. Recently a renewed interest in service composition à la Roman Model is stemming out of applications in smart manufacturing, where, through digital twins technology, manufacturing devices can export their behaviour as transition systems and hence being orchestrated very much in the same way as service did back in the early 2000's, see e.g., [8,9,10].

Interestingly, these new applications are also promoting to move from a procedural specification of the target to a declarative one, as advocated by the declarative business processes literature, through the so-called declare paradigm [11,12,13]. In other words, the target would ideally be specified in declare, and so, in Linear Temporal Logic on finite and process traces (ltl 𝑓 ) [14], with the assumption that specifications are about the possible sequence of actions (vs sequences of fluent values of the domain as in planning for ltl 𝑓 goals [15,16]), and the simplification that only one action can be selected at each point in time [11,17].

In fact, ltl 𝑓 as a specification of the target can be utilized to write two different kinds of target specification, namely process-oriented target specification or goal-oriented target specification. In the first case, very much like in the declare paradigm, one uses the ltl 𝑓 specification to specify the process itself consisting of all the traces satisfying the ltl 𝑓 formula, which in turn corresponds to implicitly specifying the transition system consisting of the deterministic finite automaton (DFA) equivalent to the ltl 𝑓 formula [14]. In this case, after a preprocessing of the ltl 𝑓 specification to obtain the target transition system (i.e., the DFA corresponding to the formula) as in [14], the composition can be performed as with the techniques used for the standard Roman Model [7].

In this paper, we study the case where ltl 𝑓 is used as a goal-oriented specification. This is a novel variant of the composition problem, where we are given a ltl 𝑓 goal, and we want to synthesize an orchestrator that, on the one hand, reactively chooses actions to form a sequence that satisfies the goal and, on the other hand, delegates each action to an available service in such a way that at any point the delegated action can be executed by the delegated service and at the end of the sequence satisfying the ltl 𝑓 formula, all services are in their final states. Specifically, we consider the available services as nondeterministic, i.e., partially controllable (similarly to FOND strong planning) as in [3,7].

Note that this problem is different from other goal-oriented service composition frameworks. In [18] Hierarchical Task Network (HTN) planning is used for service composition. HTN planning is based on the notion of composite tasks that can be refined to atomic tasks using predefined methods. While based on high-level specification of services, their approach does not support nondeterministic services. The work [19] allows the modeling of nondeterministic behaviors but not of stateful services nor high-level temporal goal specification. Authors in [20] describe services as atomic actions where only I/O behaviour is modelled, and the ontology is constituted by propositions and actions; hence services are not stateful as ours. De Giacomo et al. [21] study a stochastic version in a goal-oriented setting in which the optimization of the cost utilization is subordinated to the maximal probability of satisfaction of the goal by means of lexicographic optimization. Here instead we assume nondeterministic services.

To provide a solution technique in this case, from the ltl 𝑓 specification, we compute in linear time a symbolic representation of the corresponding Nondeterministic Finite Automaton (NFA), we do so by essentially adopting the Alternating Automaton (AFA) associated to the formula as the symbolic representation of the NFA. Then we adapt the interleaving procedure introduced in [22] to encode the symbolic NFA corresponding to ltl 𝑓 temporally extended goals into special planning actions domains. However, while in [22] considers these symbolic NFAs in deterministic planning domains, we use the technique in a nondeterministic (adversarial) planning domain that encodes all the possible service actions at each point of the computation. Notably, this is possible in our case because the target specification is an ltl 𝑓 specification of the desired sequence of target actions and not of fluent evaluation as in standard planning. Note that, the possibility of exploiting symbolic NFAs contrasts with the need of adopting DFAs required for the process-oriented target specification, which are exponentially larger than corresponding NFAs in the worst case. We implemented our approach and evaluated different heuristics and Torres and Baier's encodings to show the feasibility of our solution technique.

Although this paper has a foundational nature, our paper gives the foundations and solution techniques of goal-oriented compositions, which are indeed envisioned in the current literature on smart manufacturing where the notion of goal-oriented target specification is increasingly championed [23,8,9]. The appendix with the proofs and experimental results can be found at this link: https://bit.ly/3x5lXre.

Preliminaries

Automata theory. A deterministic finite automaton (dfa) is a tuple 𝒜 = ⟨𝒫, 𝑄, 𝑞 0 , 𝐹, 𝛿⟩ where: (i) 𝒫 is the alphabet, (ii) 𝑄 is a finite set of states, (iii) 𝑞 0 is the initial state, (iv) 𝐹 ⊆ 𝑄 is the set of accepting states and (v) 𝛿 : 𝑄 × 𝒫 → 𝑄 is a total transition function. A nondeterministic finite automaton (nfa) is defined similarly to dfa except that 𝛿 is defined as a relation, i.e. 𝛿 ⊆ 𝑄 × 𝒫 × 𝑄. An alternating finite automaton (afa) [24,25] is a generalization of dfa and nfa, where 𝛿 is defined as 𝛿 : 𝑄 × Σ → 𝐵 + (𝑄), where 𝐵 + (𝑄) is a set of positive boolean formulas whose atoms are states of 𝑄. By ℒ(𝒜), we mean the set of all traces over Σ accepted by an automaton 𝒜. An afa 𝒜 𝐴 = ⟨𝒫, 𝑄 𝐴 , 𝑞 0 , 𝐹 𝐴 , 𝛿 𝐴 ⟩ can be transformed into an equivalent nfa 𝒜 𝑁 = ⟨𝒫, 2 𝑄 𝐴 , {𝑞 0 }, 2 𝐹 𝐴 , 𝛿 𝑁 ⟩, where 𝛿 𝑁 = {(𝑞 ¯, 𝑎, 𝑞 ¯′) | 𝑞 ¯′ |= ⋀︀ 𝑞∈𝑞 ¯𝛿𝐴 (𝑞, 𝑎)}. Note that 𝒜 𝑁 can be constructed on-the-fly, see [22]. LTL 𝑓 is a variant of Linear Temporal Logic (ltl) interpreted over finite traces [14]. Given a set 𝒫 of atomic propositions, ltl 𝑓 formulas 𝜙 are defined by 𝜙 ::= 𝑎 | ¬𝜙 | 𝜙 ∧ 𝜙 | ∘ 𝜙 | 𝜙 𝒰 𝜙, where 𝑎 denotes an atomic proposition in 𝒫, ∘ is the next operator, and 𝒰 is the until operator. We use abbreviations for other Boolean connectives, as well as the following: eventually as ◇𝜙 ≡ 𝑡𝑟𝑢𝑒 𝒰 𝜙; always as □𝜙 ≡ ¬◇¬𝜙; weak next as • 𝜙 ≡ ¬ ∘ ¬𝜙 (note that, on finite traces, ¬ ∘ 𝜙 is not equivalent to ∘ ¬𝜙); and weak until as 𝜙 1 𝒲 𝜙 2 ≡ (𝜙 1 𝒰 𝜙 2 ∨ 𝜙 1 ), i.e. 𝜙 1 holds until 𝜙 2 or forever. ltl 𝑓 formulas are interpreted on finite (possibly empty) traces 𝑎 = 𝑎 0 . . . 𝑎 𝑛−1 where 𝑎 𝑖 at instant 𝑖 is a propositional interpretation over the alphabet 2 𝒫 , and 𝑛 is the length of the trace. An ltl 𝑓 formula can be transformed into an equivalent afa in linear time in the size of the formula, in a nfa in at most EXPTIME and into an equivalent and in a dfa in at most 2EXPTIME [14]. ltl 𝑓 is used in declarative process specification in BPM, through the so called DECLARE paradigm [11]. In this case it is assumed that only one proposition (corresponding to an action) is true at every time point:

𝜉 𝒫 = ( ⋁︀ 𝑎∈𝒫 𝑎) ∧ ( ⋀︀ 𝑎,𝑏∈𝒫,𝑎̸ =𝑏 𝑎 → ¬𝑏).

We call this the declare assumption, and we do adopt it in this paper. FOND Planning. A Fully-Observable Non-Deterministic (FOND) domain model can be formalized as a tuple 𝒟 = ⟨ℱ, 𝐴, pre, eff ⟩ where ℱ is a set of positive literals, 𝐴 is a set of action labels, pre and eff are two functions that define the preconditions and effects of each action 𝑎 ∈ 𝐴. A planning state 𝑠 is a subset of ℱ, and a positive literal 𝑓 holds true in 𝑠 if 𝑓 ∈ 𝑠; otherwise, 𝑓 is false in 𝑠. Both functions pre and eff take an action label 𝑎 ∈ 𝐴 as an input and return a propositional formula over ℱ and a set {eff 1 , . . . , eff 𝑛 } of effects, respectively. Each effect eff 𝑖 ∈ eff (𝑎) is a set of conditional effects each of the form 𝑐 ◁ 𝑒, where 𝑐 is a propositional formula over ℱ and 𝑒 ⊆ ℱ ∪ {¬𝑓 | 𝑓 ∈ ℱ} is a set of literals from ℱ. Sometimes we write 𝑒 as a shorthand for the unconditional effect ∅ ◁ 𝑒. An action 𝑎 can be applied in a state 𝑠 if pre(𝑎) holds true in 𝑠 (i.e., 𝑠 |= pre(𝑎)). A conditional effect 𝑐 ◁ 𝑒 is triggered in a state 𝑠 if 𝑐 is true in 𝑠. Applying 𝑎 in 𝑠 yields a successor state 𝑠 ′ determined by an outcome nondeterministically drawn from eff (𝑎). Let eff 𝑖 ∈ eff (𝑎) be the chosen nondeterministic effect, the new state 𝑠 ′ is such that ∀𝑓 ∈ ℱ, 𝑓 holds true in 𝑠 ′ if and only if either (i) 𝑓 was true in 𝑠 and no conditional effect 𝑐 ◁ 𝑒 ∈ eff 𝑖 triggered in 𝑠 deletes it (¬𝑓 ∈ 𝑒) or (ii) there is a conditional effect 𝑐 ◁ 𝑒 ∈ eff 𝑖 triggered in 𝑠 that adds it (𝑓 ∈ 𝑒). In case of conflicting effects, similarly to other works [26], we assume delete-before-adding semantics. We use 𝛿(𝑠, 𝑎) to denote the set of possible successor states {𝑠 ′ 1 , . . . , 𝑠 ′ 𝑛 } obtained by executing 𝑎 in 𝑠. Note that if 𝑠 ̸ |= pre(𝑎) then 𝛿(𝑠, 𝑎) = ∅. A FOND planning problem is a tuple Γ = ⟨𝒟, 𝑠 0 , 𝐺⟩, where 𝒟 is a domain model, 𝑠 0 ⊆ ℱ is the initial state, and 𝐺 is a formula over ℱ, also called the reachability goal. We now define what it means to solve a planning problem on 𝒟. A FOND planning problem is a tuple Γ = ⟨𝒟, 𝑠 0 , 𝐺⟩, where 𝒟 is a domain model, 𝑠 0 ⊆ ℱ is the initial state, and 𝐺 is a formula over ℱ specifying the goal states. A trace of Γ is a finite or infinite sequence 𝑠 0 , 𝑎 0 , 𝑠 1 , 𝑎 1 , . . . where 𝑠 0 is the initial state, and 𝑠 𝑖 |= pre(𝑎 𝑖 ) and 𝑠 𝑖+1 = 𝛿(𝑠 𝑖 , 𝑎 𝑖 ) for each 𝑠 𝑖 , 𝑎 𝑖 in the trace. A strategy (or plan) is a partial function 𝜋 : (2 ℱ ) + → 𝐴 such that for every 𝑢 ∈ (2 ℱ ) + , if 𝜋(𝑢) is defined then last(𝑢) |= pre(𝜋(𝑢)), i.e., it selects applicable actions. If 𝜋(𝑢) is undefined, we write 𝜋(𝑢) = ⊥. A trace 𝜏 is generated by 𝜋, or simply an 𝜋-trace, if (i) if 𝑠 0 , 𝑎 0 , . . . , 𝑠 𝑖 , 𝑎 𝑖 is a prefix of 𝜏 then 𝜋(𝑠 0 𝑠 1 . . . 𝑠 𝑖 ) = 𝑎 𝑖 , and (ii) if 𝜏 is finite, say 𝜏 = 𝑠 0 , 𝑎 0 , . . . , 𝑎 𝑛−1 , 𝑠 𝑛 , then 𝜋(𝑠 0 𝑠 1 . . . 𝑠 𝑛 ) = ⊥. A strategy 𝜋 is a (strong) solution to Γ if every 𝜋-trace is a finite trace 𝜏 such that 𝑠 𝑛 |= 𝐺.

Goal-oriented ltl 𝑓 Service Composition

Our composition framework follows the Roman model in the case the available services are nondeterministic. Unlike the Roman model, we have a high-level specification of a goal to accomplish expressed as an ltl 𝑓 formula. We want to accomplish such a goal despite the available services having nondeterministic behaviour. We detail our framework below.

Following the Roman Model [2,3,7], each (available) service is defined as a tuple 𝒮 = ⟨Σ, 𝐴, 𝜎 0 , 𝐹, 𝛿⟩ where: (i) Σ is the finite set of service states, (ii) 𝐴 is the finite set of services' actions, (iii) 𝜎 0 ∈ Σ is the initial state, (iv) 𝐹 ⊆ Σ is the set of final states (i.e., states in which the computation may stop but does not necessarily have to), and (v) 𝛿 ⊆ Σ × 𝐴 × Σ is the service transition relation. For convenience, we define 𝛿(𝜎, 𝑎) = {𝜎 ′ | (𝜎, 𝑎, 𝜎 ′ ) ∈ 𝛿}, and we assume that for each state 𝜎 ∈ Σ and each action 𝑎 ∈ 𝐴, there exist 𝜎 ′ ∈ Σ such that (𝜎, 𝑎, 𝜎 ′ ) ∈ 𝛿 (possibly 𝜎 ′ is an error state 𝜎 𝑢 that will never reach a final state). Actions in 𝐴 denote interactions between service and clients. The behavior of each available service is described in terms of a finite transition system that uses only actions from 𝐴.

Our target specification consists of a goal specification 𝜙 expressed in ltl 𝑓 over the set of propositions 𝐴. Given a community of 𝑛 services 𝒞 = {𝒮 1 , . . . , 𝒮 𝑛 }, where each set of actions 𝐴 𝑖 ⊆ 𝐴, a trace of 𝒞 is a finite or infinite alternating sequence of the form 𝑡 = (𝜎 10 . . . 𝜎 𝑛0 ), (𝑎 0 , 𝑜 0 ), (𝜎 11 . . . 𝜎 𝑛1 ), (𝑎 1 , 𝑜 1 ) . . . , where 𝜎 𝑖0 is the initial state of every service 𝒮 𝑖 and, for every 0 ≤ 𝑘, we have (i) 𝜎 𝑖𝑘 ∈ Σ 𝑖 for all 𝑖 ∈ {1, . . . , 𝑛}, (ii) 𝑜 𝑘 ∈ {1, . . . , 𝑛}, (iii) 𝑎 𝑘 ∈ 𝐴, and (iv) for all 𝑖, 𝜎 𝑖,𝑘+1 = 𝛿 𝑖 (𝜎 𝑖𝑘 , 𝑎 𝑘 ) if 𝑜 𝑘 = 𝑖, otherwise 𝜎 𝑖,𝑘+1 = 𝜎 𝑖𝑘 . Given a trace 𝑡, we call states(𝑡) the sequence of states of 𝑡, i.e. states(𝑡) = (𝜎 10 . . . 𝜎 𝑛0 ), (𝜎 11 . . . 𝜎 𝑛1 ), • • • . The choices of a trace 𝑡, denoted with choices(𝑡), is the sequence of actions in 𝑡, i.e. choices(𝑡) = (𝑎 0 , 𝑜 0 ), (𝑎 1 , 𝑜 1 ), . . . . Note that, due to nondeterminism, there might be many traces of 𝒞 associated with the same sequence of choices. Moreover, we define the action run of a trace 𝑡, denoted with actions(𝑡), the projection of choices(𝑡) only to the components in 𝐴. Note that both choices(𝑡) and actions(𝑡) are empty if 𝑡 = (𝜎 10 . . . 𝜎 𝑛0 ). A finite trace 𝑡 is successful, denoted with successful(𝑡), if (1) actions(𝑡) |= 𝜙, and (2) all service states 𝜎 𝑖 ∈ last(states(𝑡)) are such that 𝜎 𝑖 ∈ 𝐹 𝑖 .

An orchestrator is a partial function 𝛾 :

(Σ 1 × • • • × Σ 𝑛 ) + → (𝐴 × {1 . . . 𝑛}) ∪ {⊥} that, if

defined given a sequence of states 𝜎 ¯= (𝜎 10 . . . 𝜎 𝑛0 ) . . . (𝜎 1𝑚 . . . 𝜎 𝑛𝑚 ), returns the action to perform 𝑎 ∈ 𝐴, and the service (actually the service index) that will perform it; otherwise we write 𝛾(𝜎 ¯) = ⊥. Next, we define when an orchestrator is a composition that satisfies 𝜙. A trace 𝑡 is an execution of an orchestrator 𝛾 with 𝒞 if for all 𝑘 ≥ 0, we have (𝑎 𝑘 , 𝑜 𝑘 ) = 𝛾((𝜎 10 . . . 𝜎 𝑛0 ) . . . (𝜎 1𝑘 . . . 𝜎 𝑛𝑘 )) and, if 𝑡 is finite, say of length 𝑚, then 𝛾((𝜎 10 . . . 𝜎 𝑛0 ) . . . (𝜎 1,𝑚−1 . . . 𝜎 𝑛,𝑚−1 )) = ⊥. Note that due to the nondeterminism of the services, we can have many executions for the same orchestrator, despite the orchestrator being a deterministic function. We say that some finite execution 𝑡 of 𝛾 is successful, if successful(𝑡) and 𝛾(states(𝑡)) = ⊥. Finally, we say that an orchestrator 𝛾 realizes the ltl 𝑓 goal specification 𝜙 with 𝒞 if all its executions are finite traces 𝑡 that are successful. Note that the orchestrator, at every step, chooses the action and the service to which the action is delegated. In doing so, it guarantees that the sequence of actions satisfies the ltl 𝑓 goal specification and that at each step the action is delegated to a service that can actually carry out the action, despite the nondeterminism of the services. Moreover, when the orchestrator stops, all services are left in their final states. The composition problem is: Problem 1 (Composition for ltl 𝑓 Goal Specifications). Given the pair (𝒞, 𝜙), where 𝜙 is an ltl 𝑓 goal specification over the set of propositions 𝐴, and 𝒞 is a community of 𝑛 services 𝒞 = {𝒮 1 , . . . , 𝒮 𝑛 }, compute, if it exists, an orchestrator 𝛾 that realizes 𝜙. Example 1. We present an example of using our framework, inspired by the "garden bots system" example [27]. The goal is to clean the garden by picking fallen leaves and removing dirt, water the plants, and pluck the ripe fruits and flowers. The action clean must be performed at least once, followed by water and pluck in any order. In declare ltl 𝑓 , the goal can be expressed as 𝜙 = clean ∧ ∘ (clean 𝒰((water ∧ ∘ pluck ) ∨ (pluck ∧ ∘ water ))). We assume there are three available garden bots, each with different capabilities and rewards. In Figure 1 the three services specifications and the automaton 𝒜 𝜙 of the ltl 𝑓 goal 𝜙 are shown. Such an automaton 𝒜 𝜙 is a dfa in this simple case, instead of a (proper) nfa. We are interested in a composition of the bots to satisfy the goal 𝜙. Bot 1 will be used to perform clean. Although both bot 2 and 3 can be used for pluck , a strong solution cannot choose bot 2 because the action pluck can lead to the failure state 𝑏 2 ; therefore, pluck will be requested to bot 3. Bot 2 will be used for water . The order in which water and pluck are executed is irrelevant since both alternatives lead to the accepting state. Both bot 1 and bot 2 might need to be emptied to return to the initial accepting states 𝑎 0 and 𝑐 0 , respectively, and the solution must handle this.

Solution Technique

To synthesize the orchestrator, we rely on a game-theoretic technique: i.e.: (i) we build a game arena where the controller (roughly speaking the orchestrator) and the environment (the service community) play as adversaries; (ii) we synthesize a strategy for the controller to win the game whatever the environment does; (iii) from this strategy we will build the actual orchestrator.

Specifically, we proceed as follows: (1) first, from the ltl 𝑓 goal specification we compute the equivalent nfa; (2) in this nfa, we can give the control of the transition to the controller, constructing from the nfa a dfa 𝒜 act over an extended alphabet; (3) compute a product of such dfa 𝒜 act with the services, obtaining a new dfa 𝒜 𝜙,𝒞 ; (4) the latter dfa can be seen as an arena over which we play is the so-called dfa game [28]; (5) if a solution of such dfa game is found, from that solution, we can derive an orchestrator that realizes 𝜙. We now detail each step.

Step 1. The nfa 𝒜 𝜙 = (𝐴, 𝑄, 𝑞 0 , 𝐹, 𝛿) of an ltl 𝑓 formula, which can be exponentially larger than the size of the formula, can be computed by exploiting a well-known correspondence between ltl 𝑓 formulas and finite-word automata [14]. Note that we can build 𝒜 𝜙 in such a way that its alphabet is 𝐴 and not 2 𝐴 since, by the DECLARE assumption, only one action is executed at each time instant.

Step 2. From the nfa of the formula 𝜙, 𝒜 𝜙 , which is on the alphabet 𝐴, we define a controllable dfa 𝒜 act = (𝐴 × 𝑄, 𝑄, 𝑞 0 , 𝐹, 𝛿 act ) on the alphabet 𝐴 × 𝑄, with the same states, initial state and final state of 𝒜 𝜙 but with 𝛿 act defined as follows: 𝛿 act (𝑞, (𝑎, 𝑞 ′ )) = 𝑞 ′ iff (𝑞, 𝑎, 𝑞 ′ ) ∈ 𝛿. Note that the "angelic" nondeterminism of 𝒜 𝜙 is cancelled by moving the choice of the next nfa state and the next system service state in the alphabet 𝒜 × 𝑄 of the dfa 𝒜 act . Intuitively, with the dfa 𝒜 act , we are giving to the controller not only the choice of actions but also the choice of transitions of the original nfa 𝒜 𝜙 , so that those chosen transitions lead to the satisfaction of the formula. In other words, for every sequence of actions 𝑎 0 , . . . , 𝑎 𝑚−1 accepted by the nfa 𝒜 𝜙 , i.e. satisfying the formula 𝜙, there exists a corresponding alternating sequence 𝑞 0 , 𝑎 0 , . . . , 𝑞 𝑚 accepted by the dfa 𝒜 act , and viceversa.

Step 3. Then, given 𝒜 act and 𝒞, we build the composition dfa 𝒜 𝜙,𝒞 = (𝐴 ′ , 𝑄 ′ , 𝑞 ′ 0 , 𝐹 ′ , 𝛿 ′ ) as follows:

𝐴 ′ = {(𝑎, 𝑞, 𝑖, 𝜎 𝑗 ) | (𝑎, 𝑞, 𝑖, 𝜎 𝑗 ) ∈ 𝐴 × 𝑄 × {1, . . . , 𝑛} × (︀ ⋃︀ 𝑖 Σ 𝑖 )︀ and 𝜎 𝑗 ∈ Σ 𝑖 }; 𝑄 ′ = 𝑄 × Σ 1 × • • • Σ 𝑛 ; 𝑞 ′ 0 = (𝑞 0 , 𝜎 10 . . . 𝜎 𝑛0 ); 𝐹 ′ = 𝐹 × 𝐹 1 × • • • × 𝐹 𝑛 ; 𝛿 ′ ((𝑞, 𝜎 1 . . . 𝜎 𝑖 . . . 𝜎 𝑛 ), (𝑎, 𝑞 ′ , 𝑖, 𝜎 ′ 𝑖 )) = (𝑞 ′ , 𝜎 1 . . . 𝜎 ′ 𝑖 . . . 𝜎 𝑛 ) iff 𝛿 𝑖 (𝜎 𝑖 , 𝑎) = 𝜎 ′ 𝑖 ,

and 𝛿 act (𝑞, (𝑎, 𝑞 ′ )) = 𝑞 ′ . Intuitively, the dfa 𝒜 𝜙,𝒞 is a synchronous cartesian product between the nfa 𝒜 𝜙 and the service 𝒮 𝑖 chosen by the current symbol (𝑎, 𝑞, 𝑖, 𝜎) ∈ 𝐴 ′ . It can be shown that there is a relationship between the accepting runs of the dfa 𝒜 𝜙,𝒞 and the set of successful executions of some orchestrator 𝛾 with community 𝒞 for the specification 𝜙. Given a word (𝑎 0 , 𝑞 1 , 𝑜 0 , 𝜎 𝑜 0 ) . . . (𝑎 𝑚−1 , 𝑞 𝑚 , 𝑜 𝑚−1 , 𝜎 𝑜 𝑚−1 ) ∈ 𝐴 ′* , which induces the run 𝑟 = (𝑞 0 , 𝜎 10 . . . 𝜎 𝑛0 ), . . . , (𝑞 𝑚 , 𝜎 1𝑚 . . . 𝜎 𝑛𝑚 ) over 𝒜 𝜙,𝒞 , we define the history ℎ = 𝜏 𝜙,𝒞 (𝑤) = (𝜎 10 . . . 𝜎 𝑛0 ), (𝑎 0 , 𝑜 0 ), . . . , (𝜎 1𝑚 . . . 𝜎 𝑛𝑚 ). We consider the dfa 𝒜 𝜙,𝒞 as a dfa game.

Step 4. dfa games are games between two players, here called respectively the environment and the controller, that are specified by a dfa. We have a set 𝒳 of uncontrollable symbols, which are under the control of the environment, and a set 𝒴 of controllable symbols, which are under the control of the controller. A round of the game consists of both the controller and the environment choosing the symbols they control. A (complete) play is a word in 𝒳 × 𝒴 describing how the controller and environment set their propositions at each round till the game stops. A play is winning for the controller if such a play leads from the initial to a final state. A strategy for the controller is a function 𝑓 : 𝒳 * → 𝒴 that, given a history of choices from the environment, decides which symbols 𝒴 to pick next. In this context, a history has the form 𝑤 = (𝑋 0 , 𝑌 0 ) • • • (𝑋 𝑚−1 , 𝑌 𝑚−1 ). Let us denote by 𝑤 𝒳 | 𝑘 the sequence projected only on 𝒳 and truncated at the 𝑘-th element (included), i.e., 𝑤 𝒳 | 𝑘 = 𝑋 0 • • • 𝑋 𝑘 . A winning strategy is a strategy 𝑓 : 𝒳 * → 𝒴 such that for all sequences 𝑤 = (𝑋 0 , 𝑌 0 ) • • • (𝑋 𝑚−1 , 𝑌 𝑚−1 ) with 𝑌 𝑖 = 𝑓 (𝑤 𝒳 | 𝑘 ), we have that 𝑤 leads to a final state of our dfa game. The realizability problem consists of checking whether there exists a winning strategy. The synthesis problem amounts to actually computing such a strategy. A DFA game can be solved by backward least-fixpoint computation, by computing the winning region Win(𝒢), that is, the states where the controller has a winning strategy to reach a final state. First, we start with Win 0 (𝒢) = 𝐹 , and Win 𝑖 (𝒢) is the set of states for which the controller can force the game to move in a state of Win 𝑖−1 (𝒢). Let Win(𝒢) ⊆ 𝑄 be the smallest set that satisfies the winning condition. It can be shown that a DFA game 𝒢 admits a winning strategy iff 𝑠 0 ∈ Win(𝒢) [28]. The resulting strategy is a transducer 𝑇 = (𝒳 × 𝒴, 𝑄 ′ , 𝑞 ′ 0 , 𝛿 𝑇 , 𝜃 𝑇 ), defined as follows: 𝒳 × 𝒴 is the input alphabet, 𝑄 ′ is the set of states, 𝑞 ′ 0 is the initial state, 𝛿 𝑇 : 𝑄 ′ × 𝒳 → 𝑄 ′ is the transition function such that 𝛿 𝑇 (𝑞, 𝑋) = 𝛿 ′ (𝑞, (𝑋, 𝜃 𝑇 (𝑞)), and 𝜃 𝑇 : 𝑄 → 𝒴 is the output function defined as 𝜃 𝑇 (𝑞) = 𝑌 such that if 𝑞 ∈ Win 𝑖+1 (𝒢) ∖ Win 𝑖 (𝒢) then ∀𝑋.𝛿 ′ (𝑞, (𝑋, 𝑌 )) ∈ Win 𝑖 (𝒢).

Step 5. Given a strategy in the form of a transducer 𝑇 , we can obtain an orchestrator that realizes the specification. Let the extended transition function 𝛿 * 𝑇 of 𝑇 is 𝛿 * 𝑇 (𝑞, 𝜖) = 𝑞 and 𝛿 * 𝑇 (𝑞, 𝑤𝑎) = 𝛿 𝑇 (𝛿 * 𝑇 (𝑞, 𝑤), 𝑎). Then, for every sequence 𝑤 of length 𝑚 ≥ 0 𝑤 = (𝑋 0 , 𝑌 0 ) . . . (𝑋 𝑚 , 𝑌 𝑚 ), where for each index 𝑘, 𝑌 𝑘 and 𝑋 𝑘 are of the form (𝑎 𝑘 , 𝑞 𝑘+1 , 𝑜 𝑘 ) and 𝜎 𝑜 𝑘 ,𝑘 respectively, we define the orchestrator 𝛾 𝑇 ((𝜎 10 . . . 𝜎 𝑛0 ), (𝜎 11 . . . 𝜎 𝑜 1 ,1 . . . 𝜎 𝑛1 ), . . . (𝜎 1𝑚 . . . 𝜎 𝑜 𝑘 ,𝑚 . . . 𝜎 𝑛𝑚 )) = (𝑎 𝑚 , 𝑜 𝑚 ), where (𝑎 𝑚 , 𝑞 𝑚+1 , 𝑜 𝑚 ) = 𝜃 𝑇 (𝛿 * 𝑇 (𝑞 0 , 𝑤)), and whenever the trace is successful, the next choice is ⊥. Hence, we can reduce the problem of service composition for ltl 𝑓 goal specifications to solving the dfa game over 𝒜 𝜙,𝒞 with uncontrollable symbols 𝒳 = ⋃︀ 𝑖 Σ 𝑖 and controllable symbols 𝒴 = 𝐴 × 𝑄 × {1, . . . , 𝑛}. Proposition 2. 𝑎 0 . . . 𝑎 𝑚−1 ∈ ℒ(𝒜 𝜙 ) iff (𝑎 0 , 𝑞 1 ) . . . (𝑎 𝑚−1 , 𝑞 𝑚 ) ∈ ℒ(𝒜 act ), for some 𝑞 1 . . . 𝑞 𝑚 . Proposition 3. Let ℎ be a history with 𝒞 and 𝜙 be a specification. Then, ℎ is successful iff there exist a word 𝑤 ∈ 𝐴 ′* such that ℎ = 𝜏 𝜙,𝒞 (𝑤) and 𝑤 ∈ ℒ(𝒜 𝜙,𝒞 ). Proposition 3 shows that there is a tight relationship between accepting runs of 𝒜 𝜙,𝒞 and successful histories with 𝒞 for specification 𝜙. Theorem 4. Realizability for ⟨𝜙, 𝒞⟩ can be solved by checking whether 𝑞 ′ 0 ∈ Win(𝒜 𝜙,𝒞 ). Proof sketch. Soundness can be proved by induction on the maximum number of steps 𝑖 for which the controller wins the dfa game from 𝑞 ′ 0 , building 𝛾 in a backward fashion such that it chooses (𝑎 𝑘 , 𝑜 𝑘 ) ∈ 𝐴 ′ that allows forcing the win in the dfa game (which exists by assumption). Completeness can be shown by contradiction, assuming that there exists an orchestrator 𝛾 that realizes 𝜙 with community 𝒞, but that 𝑞 ′ 0 ̸ ∈ Win(𝒜 𝜙,𝒞 ), implying that we can build an arbitrarily long unsuccessful history, by definition of winning region, contradicting that 𝛾 realizes 𝜙. Theorem 5. Let the composition problem be ⟨𝜙, 𝒞⟩, and let the transducer 𝑇 be a winning strategy over the game arena 𝒜 𝜙,𝒞 . Let 𝛾 𝑇 be the orchestrator extracted from 𝑇 , as defined above. Then, 𝛾 𝑇 realizes 𝜙 with community 𝒞. Considering the cost of each step above, we get the following upper bound for the worst-case computational cost (we conjecture this cost is the exact complexity characterization): Theorem 6. Problem 1 can be solved in at most exponential time in the size of the formula, in at most exponential time in the number of services, and in polynomial time in the size of the services.

Linear Encoding in FOND Planning

In this section, we refine the solution from the previous section, taking advantage of the possibility of using FOND adversarial planning to handle the NFA corresponding to the goal symbolically in linear time. Specifically, we show how we can compute a PDDL specification that is linear in the size of the formula 𝜙, by exploiting a technique for planning for ltl 𝑓 goals in [22]. Their construction is based on representing the nfa of the goal by a symbolic representation directly stemming from the corresponding afa, and then exploring (possibly partially) the nfa on-the-fly while planning. In contrast to [22], we do this in a nondeterministic (adversarial) setting, which normally would require using dfas instead of nfas, see [15]. This is possible in our case because the ltl 𝑓 goal specifies the desired sequence of target actions, whose actual choice is under the full control of the controller that we are synthesizing.

Encoding in Adversarial FOND Planning. The game-theoretic solution technique presented in the previous section gives us the theoretical foundations for reasoning about the problem and is useful for theoretical analysis regarding the correctness and worst-case computational cost. However, the size of the game arena can be exponential in the size of the formula and exponential in the number of services, meaning that computing the entire arena beforehand may be infeasible. However, this is not required since we can build the arena on-the-fly while searching for a solution. We can do this by leveraging on FOND adversarial planning (aka strong planning in FOND), where the agent controls the actions and the environment controls the fluents [6]. In particular, we focus on planning for temporally extended goals [29,30], work on declarative and procedural constraints [31,32,33], temporal logics with finite-trace semantics, such as ltl 𝑓 [32,33,14,22], and in FOND planning [28,15,16]. More recently, [34] and [35] proposed, for classical and FOND planning, respectively, a polynomial-time compilation in PDDL for goals in Pure-Past Linear Temporal Logic (ppltl) [36]. In our setting, the orchestrator controls the actions to satisfy the ltl 𝑓 goal, while the evolution of the selected services is the uncontrollable part of the process. A forward search-based approach able to handle environment nondeterminism is, therefore, particularly interesting for our case since it could possibly avoid the exponential construction of the entire arena since the procedure stops as soon as a winning strategy is found. While the services are already given in input, the nfa 𝒜 𝜙 must be computed from the input goal specification 𝜙. To avoid constructing the entire nfa in advance, we will rely on an on-the-fly construction based on Torres and Baier's work [22]; more details later in this section. Another crucial feature of (FOND) planning is that the domain specification is assumed to be factorized, i.e., a state in the arena is a propositional assignment of a set of fluents ℱ. This feature fits well in our setting since a state of the game arena (i.e. of the composition dfa 𝒜 𝜙,𝒞 ) is made of several state components: one state component for each service, each keeping track of the current state for each service, and one component from the nfa state 𝒜 𝜙 , which keeps track of the partial satisfaction of the goal formula 𝜙.

Regarding the latter, we consider the nfa states 𝑄 𝑁 as assignments of the states of the afa 𝑄 𝐴 viewed as atomic propositions (i.e. 𝑄 𝑁 ⊆ 2 𝑄 𝐴 ) [14,22]. As for the services 𝒮 𝑖 , they also could be represented in compact (i.e. logarithmic) form with fluents ℱ 𝑖 , i.e. Σ 𝑖 = 2 ℱ 𝑖 . Indeed, one could always build a binary encoding of the state space Σ 𝑖 using log |Σ 𝑖 | bits.

Adapting Torres and Baier's Construction

Most of the techniques in FOND planning for temporal goals specify a PDDL encoding that takes a domain and a problem in PDDL with a temporal goal as input and generates new PDDL domain and problem files with a simple reachability goal. Such files can then be given in input to a (non-temporal) FOND planning solver, and the correctness of the encoding guarantees that, from a solution for the new version of the problem, we can compute a solution for the original planning problem. In our case, we adopt the encoding proposed in [22] for solving temporally-extended planning in deterministic domains. The interesting feature of their technique is that it makes it possible to encode in PDDL the construction of the nfa on-the-fly, by exploiting the relationship between afa 𝐴 𝐴 of the ltl 𝑓 formula 𝜙 and its equivalent nfa 𝐴 𝑁 . Not only is this a worst-case optimal construction in the size of the formula, but it could possibly avoid the entire construction of the nfa. The other alternatives are either superseded, not easily applicable, or worst-case non-optimal: [33]'s translation is worst-case exponential but builds the entire nfa explicitly and only works for deterministic domains; and the encoding proposed in [16] requires the construction of the entire dfa, which is not optimal since its size is doubly exponential in the size of the formula. the encoding in [35] is designed for ppltl goals, and despite ppltl and ltl 𝑓 are equally expressive, translating one into the other (and vice versa) is generally prohibitive since the best-known algorithms require 3EXPTIME [36]. Although Torres and Baier's encoding was originally used for deterministic planning domains, we observe that their construction works even in the case of nondeterministic domains, with the restriction that the propositions 𝒫 in the ltl 𝑓 goal specification are such that all are controllable by the agents and, therefore, not controllable by the environment. In fact, this is the case in our framework: we can rely on the nfa-based construction in the definition of the game arena since the nondeterminism from the nfa and the nondeterminism from the services do not directly interfere with each other. Note that if some of the propositions in the goal formula were not under the control of the agent (as is typically the case in temporally extended goals, which talk about sequences of fluent evaluations in the domain), we would end up mixing the angelic nondeterminism of the nfa with the devilish nondeterminism of the environment, and to avoid it we need determinize the nfa getting a dfa where the angelic nondeterminism has been removed. As a consequence, the complexity of planning in this case becomes 2EXPTIME-complete [15].

There are two minor issues to cope with when using Torres and Baier's encoding in our setting: (i) first, the formulas can only be evaluated over state fluents and not over actions; (ii) second, the compilation does not handle nondeterminism. In the next part, we describe how to solve these issues. First, we define the service community domain

𝒟 𝒞 = ⟨ℱ ′ , 𝐴 ′ , pre ′ , eff ′ ⟩ and problem Γ 𝒞 = ⟨𝒟 𝐶 , 𝑠 ′ 0 , 𝐺 ′ ⟩, where: (i) ℱ ′ = {start} ∪ 𝐴 ∪ Σ 1 ∪ • • • Σ 𝑛 ; (ii) 𝐴 ′ = 𝐴 × {1 . . . 𝑛}; (iii) pre ′ (⟨𝑎, 𝑖⟩) = true (since 𝛿 𝑖 are total functions); (iv) eff ′ (⟨𝑎, 𝑖⟩) = {eff ′ 𝑎,𝑖 (𝜎 𝑖1 , 𝜎 𝑖2 ) | 𝜎 𝑖2 ∈ 𝛿 𝑖 (𝜎 𝑖1 , 𝑎)} where eff ′ 𝑎,𝑖 (𝜎 𝑖1 , 𝜎 𝑖2 ) = {{𝜎 𝑖1 } ◁ {¬𝜎 𝑖1 , 𝜎 𝑖2 , 𝑎} ∪ 𝐴 ¯(𝑎)}; (v) 𝑠 ′ 0 = {start} ∪ {𝜎 𝑖0 | 𝜎 𝑖0 is the initial state of 𝒮 𝑖 }; (vi) 𝐺 ′ = {(𝜎 1 , . . . , 𝜎 𝑛 ) | 𝜎 𝑖 ∈ 𝐹 𝑖 for all 𝑖 = 1, . . . 𝑛}.

Intuitively, 𝒟 𝒞 simulates executions of 𝒞. The state induced by the fluents ℱ ′ is represented as tuples of the form (𝜎 1 , . . . , 𝜎 𝑛 , 𝑎), where 𝜎 𝑖 ∈ Σ 𝑖 and 𝑎 ∈ 𝐴. The action space 𝐴 ′ is a set of pairs of the form (𝑎, 𝑖), where 𝑎 is the chosen action and 𝑖 is the index of the chosen service that should execute it. The preconditions are not needed (though conditional effects are) since we assumed the services' transition functions are complete. The effect of action (𝑎, 𝑖) are all the possible state pairs for which there is a transition via 𝑎, but only the effects from the same current state 𝜎 𝑖1 can be triggered (see the condition), and all the successor states 𝜎 𝑖2 ∈ 𝛿 𝑖 (𝜎 𝑖1 , 𝑎) are considered (see the set comprehension for terms eff ′ 𝑎,𝑖 (𝜎 𝑖1 , 𝜎 𝑖2 )). Crucially, the action (𝑎, 𝑖) also has the effect of adding the fluent 𝑎 in the next state and removing all other action fluents; such negative effects are denoted with 𝐴 ¯(𝑎) = {¬𝑎 ′ | 𝑎 ′ ∈ 𝐴, 𝑎 ′ ̸ = 𝑎}, hence forcing the declare assumption at the semantic level. The initial state contains the auxiliary fluent start, which will be used to shift by one step the evaluation of the formula; intuitively, this is because the state-based evaluation starts from the initial state, where no action is taken yet. The auxiliary fluent start and the presence of the last action taken in the state allow us to solve the first issue. Finally, the set of goal states 𝐺 ′ corresponds to the set of services' configurations where all the states are final. The next step is to apply the translation rules specified in [22]. Given a problem instance ⟨𝜙, 𝒞⟩, and given the domain 𝒟 𝒞 and problem Γ 𝒞 as defined above, we get a new domain 𝒟 𝜙,𝒞 and problem Γ 𝜙,𝒞 by applying the translation rules with the formula 𝜙 ′ = start ∧ ∘ 𝜙. Intuitively, the evaluation of 𝜙 ′ will read the initial state and, from there on, will evaluate the chosen actions, which, by construction, are added to the subsequent states. To support nondeterminism, and so to fix the second challenge, the only change we apply is that, in "World Mode" (cfr. [22]), we consider all possible nondeterministic effects coming from 𝒟 𝒞 , i.e. eff (𝑎 ′ ) = {𝐸 ∪ {copy, ¬world} | 𝐸 ∈ eff (𝑎 ′ )}. Theorem 7. Let ⟨𝜙, 𝒞⟩ be an instance of ltl 𝑓 -goal oriented service composition. 𝜙 is realizable with 𝒞 iff there exists a strong solution for the FOND adversarial problem Γ 𝜙,𝒞 . Proof sketch. By construction of Γ 𝜙,𝒞 , and by correctness of Torres and Baier's construction, there is a one-to-one correspondence between traces of Γ 𝜙,𝒞 and the game arena 𝒜 𝜙,𝒞 (modulo deletion of the first evaluation of start). In other words, the game arena induced by 𝒟 𝜙,𝒞 and Γ 𝜙,𝒞 is essentially the same of the one induced by 𝒜 𝜙,𝒞 . Therefore, there exist a strong solution for Γ 𝜙,𝒞 iff there exist a strong solution for 𝒜 𝜙,𝒞 . The claim follows by Theorem 4. Theorem 8. ltl 𝑓 goal-oriented service composition can be solved in at most exponential time in the size of the formula, in at most exponential time in the number of services, and in polynomial time in the size of services (exponential if the service representation is in logarithmic form).

We observe that in the construction of 𝒟 𝜙,𝒞 we introduce action fluents, hence increasing the size of the state space. This could be avoided by modifying Torres and Baier's encoding with PDDL3 action-trajectory constraints [37], and hence by evaluating the temporal goal over the action-trajectory only. A detailed analysis of this option is left as future work.

Implementation and Applications

We implemented a software prototype to solve the composition problem, and we tested it on industrial case studies taken from the literature. The code can be found at https://bit.ly/3XjJbEF. The tool. Our tool takes in input a list of services (in explicit representation) and a ltl 𝑓 goal specification and computes a PDDL specification (i.e. domain and problem files) of the corresponding FOND planning task, using the technique formalized in the previous section.

First, we construct 𝒟 𝒞 and Γ 𝒞 in PDDL form. The PDDL domain file represents the nondeterministic behaviour of the services. One of the challenges we encountered was that some planning systems do not support the when expression with complex effect types, such as oneof; this prevented us from specifying the transitions as a list of when expressions, one for each possible starting state, each followed by a oneof expression that includes all the possible successors. To workaround this issue, given an action ⟨𝑎, 𝑖⟩ of 𝒟 𝒞 , we defined a PDDL operator ⟨𝑎, 𝑖, 𝜎 𝑖𝑗 ⟩, one for each possible starting state 𝜎 𝑖𝑗 ∈ Σ 𝑖 of service 𝑖; In this way, we can use the oneof effect without nesting it into a when expression.

Then, to include the on-the-fly evaluation of the ltl 𝑓 goal specification 𝜙, we rely on the [22]'s translator (in the following, denoted with TB), implemented in SWI-Prolog, to include the on-the-fly evaluation of the ltl 𝑓 goal in the planning domain. The encoding of the goal formula in PDDL follows the syntax supported by the TB translator. The TB translator supports four modes: Simple, OSA, PG, and OSA+PG, where Simple is the "naive" translation (cfr. [22], Section 4) and OSA, OSA+PG are two optimizations called "Order for Synchronization Action" and "Positive Goals" (cfr. ibid., Section 4.3). OSA+PG is the combination of OSA and PG.

The final (:goal) section includes, in conjunction: (i) the goal specified by the TB encoding, and (ii) the formula that specifies the accepting configuration for all services. Regardin (ii), the PDDL formula for the accepting service configuration has the form (and (or (curstate_s1 𝜎 11 )(curstate_s1 𝜎 12 ) . . . ) . . . (or (curstate_sn 𝜎 𝑛1 ) (curstate_sn 𝜎 𝑛2 ) . . . )), for all services 𝒮 𝑖 with 𝑖 = 1 . . . 𝑛, and 𝜎 𝑖𝑗 ∈ 𝐹 𝑖 . Intuitively, the formula captures the condition that for each service, it holds that in the current planning state each service is in either one of its final states. Note that we could have encoded the final acceptance condition by means of the formula ◇(𝜑 ∧ • true), where 𝜑 is a propositional formula, which is the formula that is accepting whenever, in the current state of the trace, 𝜑 is true. However, this would have burdened the TB translator with a larger ltl 𝑓 formula, ending up in enlarging the overhead of the encoding (i.e. more sync actions, more nfa states, etc.).

Case Studies. To test our tool, we considered case studies inspired by the literature on service composition applied to the Smart Manufacturing and Digital Twins industry.

Electric Motor (EM).

We consider a simplified version of the electric motor assembly, proposed in the context of Digital Twins composition for Smart Manufacturing [38]. The main components of an electric motor are the stator, the rotor, and, in the case of alternate current motors with direct current power (e.g., in the case of electric cars), the inverter. These three components are built or retrieved in any order, but the final assembly step must have all the previous components available. Moreover, after the assembly step, it is required that at least one test between an electric test and a full static test must be performed. This goal is captured by the following ltl 𝑓 constraints: ◇(assembleMotor ) ∧ (¬assembleMotor 𝒰 buildStator ) ∧ (¬assembleMotor 𝒰 buildRotor ) ∧ (¬assembleMotor 𝒰 buildInverter ) ∧ ◇(staticTest ∨ electricTest) ∧ (¬electricTest 𝒰 assembleMotor ) ∧ (¬staticTest 𝒰 assembleMotor ).

The 𝒰clauses prevent the assembly step before all the components are available, while the reachability goal is specified by ◇(assembleMotor ) and ◇(staticTest ∨ electricTest). We consider two types of services: infallible and breakable (Figure 2). The former has only one accepting state and supports one operation op; the latter, when executing the operation, can nondeterministically go into a "broken" state, from which a repair action is required to make it available again. In our experiments, we will have exactly one service for each process action, and scale on the number of breakable services.

Chip Production (CP).

Here we consider a smart factory scenario in which the goal is to produce chips [8]. In our simplified setting, the goal specification consists of a sequence of operations to be performed: cleaning the silicon wafers, thin film deposition, resist coating, etc. We consider three variants of this scenario, one for each service type. In particular, in the first variant, all services are of type infallible; in the second variant, they are of type breakable; and in the third variant, the services are all of type irreparable, i.e. they are like the breakable services except that they cannot be repaired. The ltl 𝑓 goal specification is a sequential goal with the following actions: cleaning, filmDeposition, resistCoating, exposure, development, etching, impuritiesImplantation, activation, resistStripping, assembly, testing, and packaging. Hence, the formula has the following form: ◇(cleaning ∧ ¬filmDeposition ∧ • • • ∧ ¬filmDeposition ∧ . . . ). Note that at each step we negate the presence of all the other. Moreover, for all variants, we will have exactly one service for each process action. We use the number of actions as a scaling parameter. Evaluation. We evaluated the MyND Planner [39], combined with the ℎ ff and ℎ max heuristics, over the PDDL files produced by our tool and the 4 available encoding of the TB translator. The metrics we considered are: pre-processing time, i.e., translation and SAS computation (TT), planning time (PT), the number of nodes expanded during the search (EN), and the policy size (PS). As benchmarks, we considered: 𝑒 𝑖 , with 𝑖 = 0, . . . , 6, are instances of the electric motor scenario with 𝑖 builder services breakable and 6 − 𝑖 infallible; 𝑐 𝑖 are the instances on the chip production scenario, with 𝑖 = 1, . . . , 12 being the length of the sequence of operations, with all services infallible; 𝑐𝑛 𝑖 as 𝑐 𝑖 but with all services breakable; and 𝑐𝑢 𝑖 as 𝑐 𝑖 but with all services irreparable. We set a timeout of 1000 seconds (≈ 15 minutes). Due to lack of space we discuss only the PT metric. Other results can be found in the appendix.

Platform. The experiments have been run on an Ubuntu 22.04 machine, endowed with 12th Gen Intel(R) Core(TM) i7-1260P, with 16 CPU threads (12 cores) and 64GB of RAM. The JVM version is 14 for compatibility with MyND. The maximum RAM for the JVM was 16GB.

Results. The results of our evaluation on all benchmarks, both using ℎ max and ℎ ff , are shown in the plots for the PT metric for each scenario: Figure 3a, 3b, 3c, and 3d. For the EM scenario (Figure 3a), we observe that the PT of the OSA encoding is generally lower than the others, and in particular ℎ max is slightly better in PT than ℎ ff . The Simple encoding has comparable but slightly higher PT. The PG encoding has the PT higher than the PT in the Simple and OSA case, for all instances, sometimes higher by a factor of 4-5. The OSA+PG encoding was considerably worse than the other since the evaluation on many instances reached the timeout. In the deterministic CP scenario (Figure 3b), we have that the OSA encoding, with respect to the PT metric, is better than the others, with no strict dominance between ℎ max and ℎ ff . The other encodings, from better to worse, were OSA+PG, PG and Simple for the ℎ ff heuristic, and Simple, PG and OSA+PG for the ℎ max heuristic. In the nondeterministic CP scenario (Figure 3c), the performances were quite worse than the deterministic case for all encodings and heuristics; the executions from cn8 on timed out. We noticed a certain advantage of using ℎ ff with the PG encoding, and ℎ max with the OSA encoding. In the unsolvable CP scenario (Figure 3d), the OSA was considerably better than the other encodings, with comparable performances between ℎ max and ℎ ff .

Discussion and Conclusion

In this paper, we have studied an advanced form of task-oriented compositions of nondeterministic services. Our goal is to synthesize an orchestrator that, using the available services, produces a trace that satisfies an ltl 𝑓 specification. To underline the importance of the ever-increasing use of service composition in smart manufacturing, we evaluate two valid case studies taken from the literature: one concerning the production of an electric motor and the other concerning the production of chips.

The tool prototype we implemented shows the feasibility of our approach. It would be interesting to test other encodings for temporal goals, such as [16] and [34,35]. This work is highly motivated by a renovated interest in service composition techniques with impactful applications in smart manufacturing [40,41,42]. In particular, the use of service composition has been advocated in an industrial scenario [10],

where the composition of a target service (manufacturing goal) is managed by means of a community of Digital Twins (manufacturing actors) modelled as stochastic services.