Composition of stochastic services for LTLf goal specifications

Conference item

Service composition à 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 (LTL_{$\mathcal{f}$}). 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 LTL_{$\mathcal{f}$}  synthesis, service composition à 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.

Authors: De Giacomo, G; Favorito, M; Silo, L

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Springer Nature
• Host title: Foundations of Information and Knowledge Systems
• Journal: Lecture Notes in Computer Science
• Volume: 14589
• Pages: 298-316
• Publication date: 2024-03-29
• Acceptance date: 2024-01-29
• Event title: 13th International Symposium, FoIKS 2024
• Event location: Sheffield, United Kingdom
• Event website: https://foiks2024.github.io/
• Event start date: 2024-04-08
• Event end date: 2024-04-11
• DOI: 10.1007/978-3-031-56940-1_17
• EISSN: 1611-3349
• ISSN: 0302-9743
• EISBN: 9783031569401
• ISBN: 9783031569395
• Language: English
• Keywords: Markov decision process; service composition; lexicographic multi-objective optimization; linear temporal logic on finite traces