Abstract
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 \(_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 \(_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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
de Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford University, USA (1997). https://searchworks.stanford.edu/view/3910936
Berardi, D., Calvanese, D., De Giacomo, G., Lenzerini, M., Mecella, M.: Automatic composition of E-services that export their behavior. In: Orlowska, M.E., Weerawarana, S., Papazoglou, M.P., Yang, J. (eds.) ICSOC 2003. LNCS, vol. 2910, pp. 43–58. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-24593-3_4
Berardi, D., Calvanese, D., De Giacomo, G., Mecella, M.: Composition of services with nondeterministic observable behavior. In: Benatallah, B., Casati, F., Traverso, P. (eds.) ICSOC 2005. LNCS, vol. 3826, pp. 520–526. Springer, Heidelberg (2005). https://doi.org/10.1007/11596141_43
Brafman, R.I., De Giacomo, G., Mecella, M., Sardiña, S.: Service composition in stochastic settings. In: Esposito, F., Basili, R., Ferilli, S., Lisi, F. (eds.) AI*IA 2017. LNCS, vol. 10640, pp. 159–171. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70169-1_12
Brafman, R.I., De Giacomo, G., Patrizi, F.: LTLf/LDLf non-Markovian rewards. In: AAAI, pp. 1771–1778. AAAI Press (2018)
Busatto-Gaston, D., Chakraborty, D., Majumdar, A., Mukherjee, S., Pérez, G.A., Raskin, J.: Bi-objective lexicographic optimization in Markov decision processes with related objectives. In: André, É., Sun, J. (eds.) ATVA 2023. LNCS, vol. 14215, pp. 203–223. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-45329-8_10
Chatterjee, K., Katoen, J.-P., Weininger, M., Winkler, T.: Stochastic games with lexicographic reachability-safety objectives. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 398–420. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53291-8_21
Chatterjee, K., Majumdar, R., Henzinger, T.A.: Markov decision processes with multiple objectives. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol. 3884, pp. 325–336. Springer, Heidelberg (2006). https://doi.org/10.1007/11672142_26
Chen, K., Xu, J., Reiff-Marganiec, S.: Markov-HTN planning approach to enhance flexibility of automatic web service composition. In: ICWS, pp. 9–16. IEEE Computer Society (2009)
Chen, Y., Huang, J., Lin, C., Shen, X.: Multi-objective service composition with QoS dependencies. IEEE Trans. Cloud Comput. (2019)
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857–907 (1995)
De Giacomo, G., Favorito, M., Leotta, F., Mecella, M., Monti, F., Silo, L.: AIDA: a tool for resiliency in smart manufacturing. In: Cabanillas, C., Pérez, F. (eds.) CAiSE 2023. LNBIP, vol. 477, pp. 112–120. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-34674-3_14
De Giacomo, G., Favorito, M., Leotta, F., Mecella, M., Silo, L.: Digital twins composition via Markov decision processes. In: ITBPM@BPM. CEUR Workshop Proceedings, vol. 2952, pp. 44–49. CEUR-WS.org (2021)
De Giacomo, G., Favorito, M., Leotta, F., Mecella, M., Silo, L.: Modeling resilient cyber-physical processes and their composition from digital twins via Markov decision processes. In: PMAI@IJCAI. CEUR Workshop Proceedings, vol. 3310, pp. 101–104. CEUR-WS.org (2022)
De Giacomo, G., Favorito, M., Leotta, F., Mecella, M., Silo, L.: Digital twin composition in smart manufacturing via Markov decision processes. Comput. Ind. 149, 103916 (2023)
De Giacomo, G., Mecella, M., Patrizi, F.: Automated service composition based on behaviors: the roman model. In: Bouguettaya, A., Sheng, Q., Daniel, F. (eds.) Web Services Foundations, pp. 189–214. Springer, New York (2014). https://doi.org/10.1007/978-1-4614-7518-7_8
De Giacomo, G., Patrizi, F., Sardina, S.: Automatic behavior composition synthesis. Artif. Intell. 196, 106–142 (2013)
De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: IJCAI, pp. 854–860. IJCAI/AAAI (2013)
Di Ciccio, C., Montali, M.: Declarative process specifications: reasoning, discovery, monitoring. In: van der Aalst, W.M.P., Carmona, J. (eds.) Process Mining Handbook. Lecture Notes in Business Information Processing, vol. 448, pp. 108–152. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-08848-3_4
Dumas, M., et al.: AI-augmented business process management systems: a research manifesto. ACM Trans. Manag. Inf. Syst. 14(1), 11:1–11:19 (2023)
Gao, A., Yang, D., Tang, S., Zhang, M.: Web service composition using Markov decision processes. In: Fan, W., Wu, Z., Yang, J. (eds.) WAIM 2005. LNCS, vol. 3739, pp. 308–319. Springer, Heidelberg (2005). https://doi.org/10.1007/11563952_28
Hahn, E.M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A., Wojtczak, D.: Model-free reinforcement learning for lexicographic omega-regular objectives. In: Huisman, M., Păsăreanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 142–159. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-90870-6_8
Hensel, C., Junges, S., Katoen, J., Quatmann, T., Volk, M.: The probabilistic model checker storm. Int. J. Softw. Tools Technol. Transf. 24(4), 589–610 (2022)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47
Marrella, A., Mecella, M., Sardiña, S.: Supporting adaptiveness of cyber-physical processes through action-based formalisms. AI Commun. 31(1), 47–74 (2018)
Monti, F., Silo, L., Leotta, F., Mecella, M.: On the suitability of AI for service-based adaptive supply chains in smart manufacturing. In: ICWS, pp. 704–706. IEEE (2023)
Monti, F., Silo, L., Leotta, F., Mecella, M.: Services in smart manufacturing: comparing automated reasoning techniques for composition and orchestration. In: Aiello, M., Barzen, J., Dustdar, S., Leymann, F. (eds.) SummerSOC 2023. CCIS, vol. 1847, pp. 69–83. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-45728-9_5
Moustafa, Ahmed, Zhang, Minjie: Multi-objective service composition using reinforcement learning. In: Basu, Samik, Pautasso, Cesare, Zhang, Liang, Fu, Xiang (eds.) ICSOC 2013. LNCS, vol. 8274, pp. 298–312. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-45005-1_21
Papazoglou, M.P., Traverso, P., Dustdar, S., Leymann, F.: Service-oriented computing: state of the art and research challenges. Computer 40(11), 38–45 (2007)
Pesic, M., Schonenberg, H., Van der Aalst, W.M.: Declare: full support for loosely-structured processes. In: EDOC (2007)
Puterman, M.L.: Markov decision processes (1994)
Sadeghiram, S., Ma, H., Chen, G.: A user-preference driven lexicographic approach for multi-objective distributed web service composition. In: 2020 IEEE Symposium Series on Computational Intelligence (SSCI) (2020)
Skalse, J., Abate, A.: On the limitations of Markovian rewards to express multi-objective, risk-sensitive, and modal tasks. In: UAI. Proceedings of Machine Learning Research, vol. 216, pp. 1974–1984. PMLR (2023)
Skalse, J., Hammond, L., Griffin, C., Abate, A.: Lexicographic multi-objective reinforcement learning. In: IJCAI, pp. 3430–3436. ijcai.org (2022)
Wells, A.M., Lahijanian, M., Kavraki, L.E., Vardi, M.Y.: LTLf synthesis on probabilistic systems. In: GandALF. EPTCS, vol. 326 (2020)
Wray, K., Zilberstein, S., Mouaddib, A.I.: Multi-objective MDPs with conditional lexicographic reward preferences. In: AAAI (2015)
Yadav, N., Sardiña, S.: Decision theoretic behavior composition. In: AAMAS, pp. 575–582. IFAAMAS (2011)
Acknowledgements
This work has been partially supported by the EU H2020 project AIPlan4EU (No. 101016442), the ERC-ADG WhiteMech (No. 834228), the EU ICT-48 2020 project TAILOR (No. 952215), the PRIN project RIPER (No. 20203FFYLK), and the PNRR MUR project FAIR (No. PE0000013). This work has been carried out while Luciana Silo was enrolled in the Italian National Doctorate on Artificial Intelligence run by Sapienza University of Rome.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
De Giacomo, G., Favorito, M., Silo, L. (2024). Composition of Stochastic Services for LTL\(_f\) Goal Specifications. In: Meier, A., Ortiz, M. (eds) Foundations of Information and Knowledge Systems. FoIKS 2024. Lecture Notes in Computer Science, vol 14589. Springer, Cham. https://doi.org/10.1007/978-3-031-56940-1_17
Download citation
DOI: https://doi.org/10.1007/978-3-031-56940-1_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-56939-5
Online ISBN: 978-3-031-56940-1
eBook Packages: Computer ScienceComputer Science (R0)