1. Introduction
The service-oriented computing (SOC) paradigm uses services to support the development
of rapid, low-cost, interoperable, evolvable, and massively distributed applications. Services
are considered autonomous, platform-independent entities that can be described, published,
discovered, and loosely coupled in novel ways [
1
]. Service composition, i.e. the ability to
generate new, more useful services from existing ones, is an active field of research in the
SOC area and has been actively investigated for over a decade. Particularly interesting in this
context is the so-called Roman Model [
2, 3, 4, 5
] where services are conversational, i.e., have an
internal state and are modeled as finite state machines (FSM), where at each state the service
ofers 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, from the set of existing
services specified using an FSM, too. The goal is to see whether the target can be satisfied by
properly orchestrating the work of the component service and building a scheduler called the
orchestrator that will use actions provided by existing services to implement action requests.
In this paper, we consider a variant of the Roman Model where the composition is
taskoriented, and this makes it more similar to Planning in AI [
6, 7, 8
]. Specifically, we are given
a task, and we want to synthesize an orchestrator that, on the one hand, reactively chooses
actions to form a sequence that satisfies the task and, on the other hand, delegates each action
to an available service in such a way that at the end of the sequence, all services are in their
ifnal states. We consider the available services as nondeterministic, in the sense that when the
orchestrator delegates to them an action, they will change state in a nondeterministic (devilish
vs. angelic) way, as studied, e.g. in [
3
]. We draw from the work on declarative process modeling
in Business Process Management (BPM) in which the task specification is expressed in Linear
Temporal Logic on finite traces ( ltl ) [
9
] with the so-called declare assumption that only one
action can be selected at each point in time [
10
]. This gives us a rich way to specify dynamic
tasks that extend over time. We give a formal definition of composition and a provably correct
technique to actually solve the composition problem and obtain the orchestrator. The technique
is readily implementable. The solution technique is based on finding a winning strategy for
a two-player game over a particular dfa game, as done, for example, in ltl synthesis [
11
].
Although this paper has a foundational nature, we observe that these kinds of task-oriented
compositions are increasingly becoming important in smart manufacturing [
12
].
2. Composition of Nondeterministic Services for LTL Tasks
In this section we present our service composition in the case the available service are
nondeterministic. Unlike the classical Roman model, we do not have an explicit specification of the
target service to realize, but rather, a high-level specification of a task to accomplish expressed
as an ltl formula.
2.1. Nondeterministic Services Framework
In the Roman Model [
2
], each (available) service is defined as a tuple = ⟨Σ , , 0, , ⟩
formed respectively by: a finite set Σ of service states, a finite set of services’ actions, an
initial state 0, a set of final states (i.e., states in which the computation may stop, but does
not necessarily have to), and a 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 behaviour of
each available service is described in terms of a finite transition system that uses only actions
from . Consider a task specification expressed in ltl over the set of propositions , and
consider a community of services = {1, . . . , }. An infinite trace of is an infinite
alternating sequence of the form = ( 10 . . . 0), (1, 1), ( 11 . . . 1), (2, 2) . . . where
for every 0 ≤ , we have (i) ∈ Σ for all ∈ {1, . . . , }, (ii) ∈ {1, . . . , }, (iii) ∈ ,
and (iv) for all , ,+1 = ( , +1) if +1 = , and ,+1 = otherwise. A history of
is a finite prefix of a trace of . Given a trace , we call states() 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() = (1, 1), (, ), . . . . Moreover, we define
the action run of a trace , denoted with actions(), the projection of choices() only to the
components in . Due to nondeterminism, there might be many traces of associated with the
same action run. states, choices and actions are defined also on history ℎ, in a similar way.
An orchestrator is a function : (Σ 1 × · · · × Σ )* → × { 1 . . . } that, given a sequence
of states, returns the action to perform, and the service (actually the service index) that will
perform it. Given a trace , with histories(), we denote the set of prefixes of the trace that
ends with a services state configuration. A trace is an execution of an orchestrator over
if for all ≥ 0, we have (+1, +1) = (( 10 . . . 0) . . . ( 1 . . . )). If we consider
, be the set of such executions we can have many executions for the same orchestrator,
despite the orchestrator being a deterministic function (due nondeterminism of the services). If
ℎ ∈ histories() for some (infinite) execution ∈ , , we call ℎ a finite execution of over .
We say that some finite execution ℎ is successful, denoted with successful(ℎ), if the following
two conditions hold: (1) actions(ℎ) |= , and (2) all service state ∈ last(states(ℎ)) are such
that ∈ . If for execution ∈ , there exist a finite prefix history ℎ ∈ histories() such
that successful(ℎ), we say that is successful. Finally, we say that an orchestrator realizes the
ltl specification with if, for all traces ∈ , , is successful. Since the orchestrator at
every step chooses the action and the (index of the) service to which the action is delegated, it
guarantees the (complete) sequence of actions that satisfy the ltl task specification. Hence,
when the orchestrator stops, all services are left in their final states.
The composition problem is: given the pair (, ), where is an ltl task specification over
the set of propositions , and is a community of services = {1, . . . , }, compute, if it
exists, an orchestrator that realizes .
2.2. Nondeterministic Services Solution Technique
To synthesize the orchestrator we rely on a game-theoretic technique: (i) we build a game
arena where the controller (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 according to the following steps.
Step (1) First, from the ltl task specification we compute the equivalent Nondeterministic
Finite Automaton (nfa) of an ltl formula = (, , 0, , ) using the ltl 2nfa algorithm
[
13
]. Only one action is executed at each time instant.
Step (2) From this nfa we define a controllable Deterministic Finite Automaton (dfa) on the
alphabet × , act = ( × , , 0, , act), where everything is as in except act, with
which can give the control of the transition to the controller. This means that for every sequence
of actions 1, . . . , accepted by the nfa , there exists a corresponding alternating sequence
0, 1, . . . , accepted by the dfa act, and viceversa. In other words, when we project out the
-component from the accepted sequences of act, we get a sequence of actions satisfying .
Step (3) Then, we compute the product of such dfa act with the services, obtaining the
composition dfa , again extending the alphabet with new symbols, which this time are
under the control of the environment. Intuitively, the dfa , over alphabet ′ is a
synchronous cartesian product between the nfa and the service chosen by the current
symbol (, , , ) ∈ ′. The “angelic” nondeterminism of and the “devilish”
nondeterminism coming from the services is cancelled by moving the choice of the next nfa state and the
next system service state in the alphabet ′. 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
over community for the specification .
Step (4) The dfa obtained is the arena over which we play the so-called dfa game [
11
]. It is
a game between two players: the environment and the controller. is the set of uncontrollable
symbols (under the control of the environment), is the set of controllable symbols (under
the control of the controller). This is a classical problem and can be solved as follows. First,
we define the controllable preimage (ℰ ) of a set ℰ of states of as the set of states
s.t. there exists a choice for symbols s.t. for all choices of symbols , game progresses
to states in ℰ . Then, we define the set Win() of winning states of a dfa game , i.e., the
set formed by the states from which the controller can win the DFA game . Specifically,
Win() is defined as the least-fixpoint, making use of approximates Win() denoting all
states where the controller wins in at most steps: (1) Win0() = (the final states of );
and (2) Win+1() = Win() ∪ PreC (Win()). Then, Win() = ⋃︀ Win().
Computing Win() requires linear time in the number of states in . Indeed, after at most a
linear number of steps Win+1() = Win() = Win(). It can be shown that a DFA
game admits a winning strategy if 0 ∈ Win(), and the resulting strategy is a transducer
= ( × , ′, 0′, , ) formed by: the input alphabet × , the set of states ′, the
initial state 0′, the transition function : ′ × → ′ s.t. (, ) = ′(, (, ()), and
: → is the output function defined as () = s.t. if ∈ Win+1() ∖ Win()
then ∀. (, (, )) ∈ Win() [
11
]. Given a strategy in the form of a transducer ,
we can obtain an orchestrator that realizes the specification as follows. Let the extended
transition function * of is * (, ) = and * (, ) = ( * (, ), ). Then, for
every sequence of length ≥ 0 = (1, 1) . . . (, ), where for each index ,
and are of the form (, , ) and , respectively, we define the orchestrator
(( 10 . . . 0), ( 11 . . . 1,1 . . . 1), . . . ( 1 . . . , . . . )) = (+1, +1), where
(+1, +1, +1) = ( * (0, )). We can reduce the problem of service composition
for ltl task specifications to solving the dfa game over , with uncontrollable symbols
= ⋃︀ Σ and controllable symbols = × × { 1, . . . , }. It can be shown that the
service composition realizability problem with community for the satisfaction of an ltl task
specification can be solved by checking whether 0′ ∈ Win(, ), and that the problem 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.