  In this paper, we study the composition of services so as to obtain runs
satisfying a task specification in Linear Temporal Logic on finite traces
(LTLf). We study the problem in the case services are nondeterministic and the
LTLf specification can be exactly met, and in the case services are stochastic,
where we are interested in maximizing the probability of satisfaction of the
LTLf specification and, simultaneously, minimizing the utilization cost of the
services. To do so, we combine techniques from LTLf synthesis, service
composition \`a la Roman Model, reactive synthesis, and bi-objective
lexicographic optimization on MDPs. This framework has several interesting
applications, including Smart Manufacturing and Digital Twins.
