Composition of Stochastic Services for LTLf Goal Specifications

Service composition a la Roman model consists of realizing a virtual service by orchestrating suitably a set of already available services. In this paper, we consider a variant where available services are stochastic systems, and the target specification is goal-oriented and specified in Linear Temporal Logic on finite traces (LTLf ). In this setting, we are interested in synthesizing a controller (policy) that maximizes the probability of satisfaction with the goal, while minimizing the expected cost of the utilization of the available services. To do so, we combine techniques from LTLf synthesis, service composition a la Roman Model, reactive synthesis, and bi-objective lexicographic optimization on Markov Decision Processes (MDPs). This framework has several interesting applications, including Smart Manufacturing and Digital Twins.