Composition of Nondeterministic and Stochastic Services for LTLf Task Specifications
This work addresses service composition for task automation in domains like Smart Manufacturing and Digital Twins, representing an incremental advancement by integrating existing techniques.
The paper tackles the problem of composing nondeterministic and stochastic services to satisfy Linear Temporal Logic on finite traces (LTLf) task specifications, achieving exact satisfaction for nondeterministic services and maximizing probability while minimizing cost for stochastic services.
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 à la Roman Model, reactive synthesis, and bi-objective lexicographic optimization on MDPs. This framework has several interesting applications, including Smart Manufacturing and Digital Twins.