Composition of stochastic services for LTLf goal specifications
Service composition <i>à la</i> 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 speci...
| Main Authors: | , , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
Springer Nature
2024
|
| _version_ | 1826312933855985664 |
|---|---|
| author | De Giacomo, G Favorito, M Silo, L |
| author_facet | De Giacomo, G Favorito, M Silo, L |
| author_sort | De Giacomo, G |
| collection | OXFORD |
| description | Service composition <i>à la</i> 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<sub>$\mathcal{f}$</sub>). 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<sub>$\mathcal{f}$</sub> synthesis, service composition <i>à la</i> 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. |
| first_indexed | 2024-04-23T08:25:05Z |
| format | Conference item |
| id | oxford-uuid:19ca0d94-1ea2-479c-995a-1088af327a0d |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-09-25T04:03:04Z |
| publishDate | 2024 |
| publisher | Springer Nature |
| record_format | dspace |
| spelling | oxford-uuid:19ca0d94-1ea2-479c-995a-1088af327a0d2024-05-10T17:05:04ZComposition of stochastic services for LTLf goal specificationsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:19ca0d94-1ea2-479c-995a-1088af327a0dEnglishSymplectic ElementsSpringer Nature2024De Giacomo, GFavorito, MSilo, LService composition <i>à la</i> 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<sub>$\mathcal{f}$</sub>). 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<sub>$\mathcal{f}$</sub> synthesis, service composition <i>à la</i> 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. |
| spellingShingle | De Giacomo, G Favorito, M Silo, L Composition of stochastic services for LTLf goal specifications |
| title | Composition of stochastic services for LTLf goal specifications |
| title_full | Composition of stochastic services for LTLf goal specifications |
| title_fullStr | Composition of stochastic services for LTLf goal specifications |
| title_full_unstemmed | Composition of stochastic services for LTLf goal specifications |
| title_short | Composition of stochastic services for LTLf goal specifications |
| title_sort | composition of stochastic services for ltlf goal specifications |
| work_keys_str_mv | AT degiacomog compositionofstochasticservicesforltlfgoalspecifications AT favoritom compositionofstochasticservicesforltlfgoalspecifications AT silol compositionofstochasticservicesforltlfgoalspecifications |