Service composition for LTLf task specifications

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 à la Roman Model, where the goals specified allowed traces declaratively via Linear Temporal Logic on finite traces (LTLf). Specifically, we synthesize a controller to orchestrate the available services to produce a trace satisfying a specification in LTLf. We demonstrate that this framework has several interesting applications, like Smart Manufacturing and Digital Twins.