LTLf Goal-oriented Service Composition

Service compositions à la Roman model consist of realizing a virtual service by orchestrating suitably a set of already available services, where all services are described procedurally as (possibly nondeterministic) transition systems. In this paper, we study a goal-oriented variant of the service composition \emph{à la} Roman Model, where the goal specifies the allowed traces declaratively via Linear Temporal Logic on finite traces (LTLf). Specifically, we want to synthesize a controller to orchestrate the available services to produce together a trace satisfying a specification in LTLf. To do so, we combine techniques from reactive synthesis, FOND Planning, and the Roman Model for service composition. This framework has several interesting applications, including Smart Manufacturing and Digital Twins.