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.

翻译：本文研究如何通过服务组合获得满足有限迹线性时序逻辑（LTLf）任务规范的运行轨迹。我们探讨了两类场景：非确定性服务可精确满足LTLf规范的情形，以及随机服务中需同时最大化LTLf规范满足概率与最小化服务使用成本的情形。为此，融合了LTLf综合、罗马型服务组合、反应式综合以及马尔可夫决策过程双目标词典优化等技术。该框架在智能制造、数字孪生等领域具有重要应用价值。