Service compositions à la Roman model consist of realizing a virtual service by orchestrating suitably a set of already available services, where all services are described procedurally as (possibly nondeterministic) transition systems. In this paper, we study a goal-oriented variant of the service composition à la Roman Model, where the goal specifies the allowed traces declaratively via Linear Temporal Logic on finite traces ( ltl ). Specifically, we want to synthesize a controller to orchestrate the available services to produce together a trace satisfying a specification in ltl . To do so, we combine techniques from reactive synthesis, FOND Planning, and the Roman Model for service composition. This framework has several interesting applications, including Smart Manufacturing and Digital Twins.
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
lfexibility 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 [
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., [
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 [
In fact, ltl as a specification of the target can be utilized to write two diferent 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 [
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 [
Note that this problem is diferent 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 diferent 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 [
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 [
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 efects 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 efects, respectively. Each efect eff ∈ eff () is a set of conditional efects 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 efect ∅ ◁ . An action can be applied in a state if pre() holds true in (i.e., |= pre()). A conditional efect ◁ 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 efect, the new state ′ is such that ∀ ∈ ℱ , holds true in ′ if and only if either (i) was true in and no conditional efect ◁ ∈ eff triggered in deletes it (¬ ∈ ) or (ii) there is a conditional efect ◁ ∈ eff triggered in that adds it ( ∈ ). In case of conflicting efects, 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 (01 . . . ) = , and (ii) if is finite, say = 0, 0, . . . , − 1, , then (01 . . . ) = ⊥. A strategy is a (strong) solution to Γ if every -trace is a finite trace such that |= . 3. 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 [
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 diferent 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. tccboahonoWtpsobeestreeofauobrssroeaemttdii2nscffotblyeereracptenhalsuue.tecsAgedkol,ttiahhanleosautar.gccothBoniomgobntospop1tohllsuuwibtctiiioklooltnncb2aceonaafunnlesntdheaodd3et ℬlecan1 10 cleteypmanem1pℬtyw2aplutcekr0 pwlucakte⊤2r ℬlckpu3 10 teypmcleanlcean10pwluatcerk32 pwluactek4r ⊤ to the failure state 2; therefore, pluck will be requested to bot 3. Bot 2 will be used for water . Figure 1: From left to right: the three available bots The order in which water and pluck are exe- of the garden bot systems, and the automacuted is irrelevant since both alternatives lead ton of the ltl goal. 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.
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 [
Step 3. Then, given act and , we build the composition dfa , = (′, ′, 0′, ′, ′) as follows: ′ = {(, , , ) | (, , , ) ∈ × × { 1, . . . , } × ︀( ⋃︀ Σ ︀) and ∈ Σ }; ′ = × Σ 1 × · · · Σ ; 0′ = (0, 10 . . . 0); ′ = × 1 × · · · × ; ′((, 1 . . . . . . ), (, ′, , ′)) = (′, 1 . . . ′ . . . ) if ( , ) = ′, 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 Win0() = , 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 if 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 ∈ ℒ( ) if (0, 1) . . . (− 1, ) ∈ ℒ(act), for some 1 . . . . Proposition 3. Let ℎ be a history with and be a specification. Then, ℎ is successful if 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.
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 [
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 ifles 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 efects are) since we assumed the services’ transition functions are complete. The efect of action (, ) are all the possible state pairs for which there is a transition via , but only the efects 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 efect of adding the fluent in the next state and removing all other action fluents; such negative efects 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 efects coming from , i.e. eff (′) = { ∪ {copy, ¬world} | ∈ eff (′)}.
Theorem 7. Let ⟨, ⟩ be an instance of ltl -goal oriented service composition. is realizable with if 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 Γ , if 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.
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 efect 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 efect 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:
Electric motor scenario
0 e0 e1 e2#breakabel3eservices e4 e5 e6 0 c1 c2 c3 c4 c5lengtch6offocr7mulac8 c9 c10 c11 c12 0 cn1 cn2 cn3 cn4 cn5lengtchn6offocnrm7ulacn8 cn9 cn10 cn11 cn12 0 cu1 cu2 cu3 cu4 cu5lengtchu6offocurm7ulacu8 cu9 cu10 cu11 cu12
(a) PT metric for the EM (b) PT metric for the CP sce- (c) PT metric for the CP sce-(d) PT metric for the CP
scescenario. nario (det). nario (nondet). nario (unsolvable).
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 pro- op op op
duce chips [
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 .
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 [
J. Artif. Intell. Res. 63 (2018) 557–623. [18] E. Sirin, B. Parsia, D. Wu, J. A. Hendler, D. S. Nau, HTN planning for web service composition using SHOP2, J. Web Semant. (2004). [19] J. Alves, J. Marchi, R. Fileto, M. A. R. Dantas, Resilient composition of web services through nondeterministic planning, in: ISCC, 2016. [20] M. Pistore, A. Marconi, P. Bertoli, P. Traverso, Automated composition of web services by planning at the knowledge level, in: IJCAI, 2005. [21] G. De Giacomo, M. Favorito, L. Silo, Composition of stochastic services for ltlf goal specifications, in: FoIKS, 2024. [22] J. Torres, J. A. Baier, Polynomial-time reformulations of LTL temporally extended goals into ifnal-state goals, in: IJCAI, 2015. [23] A. Marrella, M. Mecella, S. Sardiña, Supporting adaptiveness of cyber-physical processes through action-based formalisms, AI Commun. (2018). [24] A. K. Chandra, D. Kozen, L. J. Stockmeyer, Alternation, J. ACM (1981). [25] M. Y. Vardi, An automata-theoretic approach to linear temporal logic, 1995. [26] G. Röger, F. Pommerening, M. Helmert, Optimal Planning in the Presence of Conditional Efects:
Extending LM-Cut with Context Splitting, in: ECAI, 2014. [27] N. Yadav, S. Sardina, Decision theoretic behavior composition, in: AAMAS, 2011. [28] G. De Giacomo, M. Y. Vardi, Synthesis for LTL and LDL on finite traces, in: IJCAI, 2015. [29] F. Bacchus, F. Kabanza, Planning for temporally extended goals, Ann. Math. Artif. Int. (1998). [30] F. Bacchus, F. Kabanza, Using temporal logics to express search control knowledge for planning,
Artif. Intell. (2000). [31] J. A. Baier, C. Fritz, M. Bienvenu, S. A. McIlraith, Beyond classical planning: Procedural control knowledge and preferences in state-of-the-art planners, in: AAAI, 2008. [32] J. A. Baier, S. A. McIlraith, Planning with first-order temporally extended goals using heuristic search, in: AAAI, 2006. [33] J. A. Baier, S. A. McIlraith, Planning with temporally extended goals using heuristic search, in:
ICAPS, 2006. [34] L. Bonassi, G. De Giacomo, M. Favorito, F. Fuggitti, A. E. Gerevini, E. Scala, Planning for temporally extended goals in pure-past linear temporal logic, in: ICAPS, 2023. [35] L. Bonassi, G. De Giacomo, M. Favorito, F. Fuggitti, A. E. Gerevini, E. Scala, FOND planning for pure-past linear temporal logic goals, in: ECAI, 2023. [36] G. De Giacomo, A. Di Stasio, F. Fuggitti, S. Rubin, Pure-past linear temporal and dynamic logic on ifnite traces, in: IJCAI, 2020. [37] L. Bonassi, A. E. Gerevini, E. Scala, Planning with qualitative action-trajectory constraints in
PDDL, in: IJCAI, 2022. [38] G. De Giacomo, M. Favorito, F. Leotta, M. Mecella, F. Monti, L. Silo, AIDA: A tool for resiliency in smart manufacturing, in: CAiSE Forum, 2023. [39] R. Mattmüller, Informed progression search for fully observable nondeterministic planning, Ph.D.
thesis, 2013. [40] T. Catarci, D. Firmani, F. Leotta, F. Mandreoli, M. Mecella, F. Sapio, A conceptual architecture and model for smart manufacturing relying on service-based digital twins, in: ICWS, 2019. [41] G. De Giacomo, P. Felli, B. Logan, F. Patrizi, S. Sardiña, Situation calculus for controller synthesis in manufacturing systems with first-order state representation, Artif. Intell. (2022). [42] G. De Giacomo, M. Y. Vardi, P. Felli, N. Alechina, B. Logan, Synthesis of orchestrations of transducers for manufacturing, in: AAAI, 2018.