{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T04:45:13Z","timestamp":1778215513211,"version":"3.51.4"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031479625","type":"print"},{"value":"9783031479632","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-47963-2_9","type":"book-chapter","created":{"date-parts":[[2023,11,22]],"date-time":"2023-11-22T21:41:26Z","timestamp":1700689286000},"page":"119-138","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Dynamic Temporal Logic for\u00a0Quality of\u00a0Service in\u00a0Choreographic Models"],"prefix":"10.1007","author":[{"given":"Carlos G. Lopez","family":"Pombo","sequence":"first","affiliation":[]},{"given":"Agust\u00edn E. Martinez","family":"Su\u00f1\u00e9","sequence":"additional","affiliation":[]},{"given":"Emilio","family":"Tuosto","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,11,23]]},"reference":[{"key":"9_CR1","unstructured":"Obj. Mgmt. Group: Business Process Model and Notation. http:\/\/www.bpmn.org"},{"key":"9_CR2","volume-title":"Reactive Microsystems - The Evolution Of Microservices At Scale","author":"J Bon\u00e9r","year":"2018","unstructured":"Bon\u00e9r, J.: Reactive Microsystems - The Evolution Of Microservices At Scale. O\u2019Reilly, Newton (2018)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Frittelli, L., Maldonado, F., Melgratti, H.C., Tuosto, E.: A choreography-driven approach to apis: the opendxl case study. In: [4], 107\u2013124 (2020)","DOI":"10.1007\/978-3-030-50029-0_7"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-50029-0","volume-title":"Coordination Models and Languages","year":"2020","unstructured":"Bliudze, S., Bocchi, L. (eds.): COORDINATION 2020. LNCS, vol. 12134. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-50029-0"},{"issue":"1","key":"9_CR5","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1109\/MS.2014.131","volume":"32","author":"M Autili","year":"2015","unstructured":"Autili, M., Inverardi, P., Tivoli, M.: Automated synthesis of service choreographies. IEEE Softw. 32(1), 50\u201357 (2015)","journal-title":"IEEE Softw."},{"key":"9_CR6","unstructured":"World Wide Web Consortium: Web services description language (wsdl) version 2.0 part 1: Core language. https:\/\/www.w3.org\/TR\/wsdl20\/"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Ivanovi\u0107, D., Carro, M., Hermenegildo, M.V.: A constraint-based approach to quality assurance in service choreographies. In: Liu, C., et al. (eds.) Proceedings of SOC, pp. 252\u2013267 (2012)","DOI":"10.1007\/978-3-642-34321-6_17"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Kattepur, A., Georgantas, N., Issarny, V.: QoS analysis in heterogeneous choreography interactions. In: Basu, S., et al. (eds.) Proceedings of SOC, pp. 23\u201338 (2013)","DOI":"10.1007\/978-3-642-45005-1_3"},{"issue":"4","key":"9_CR9","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1109\/TSC.2015.2413401","volume":"9","author":"M G\u00fcdemann","year":"2016","unstructured":"G\u00fcdemann, M., Poizat, P., Sala\u00fcn, G., Ye, L.: VerChor: a framework for the design and verification of choreographies. IEEE Trans. Serv. Comput. 9(4), 647\u2013660 (2016)","journal-title":"IEEE Trans. Serv. Comput."},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-030-22397-7_6","volume-title":"Coordination Models and Languages","author":"M Autili","year":"2019","unstructured":"Autili, M., Di Salle, A., Gallo, F., Pompilio, C., Tivoli, M.: CHOReVOLUTION: automating the realization of highly\u2013collaborative distributed applications. In: Riis Nielson, H., Tuosto, E. (eds.) COORDINATION 2019. LNCS, vol. 11533, pp. 92\u2013108. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-22397-7_6"},{"key":"9_CR11","unstructured":"Bocchi, L., Melgratti, H.C., Tuosto, E.: On resolving non-determinism in choreographies. Log. Methods Comput. Sci. 16(3) (2020)"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Basu, S., Bultan, T., Ouederni, M.: Deciding choreography realizability. In: Field, J., et al. (eds.) Proceedings of the 39th ACM SIGPLAN-SIGACT POPL 2012, pp. 191\u2013202. ACM (2012)","DOI":"10.1145\/2103656.2103680"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"H\u00fcttel, H., et al.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3:1\u20133:36 (2016)","DOI":"10.1145\/2873052"},{"issue":"2","key":"9_CR14","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D Brand","year":"1983","unstructured":"Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323\u2013342 (1983)","journal-title":"J. ACM"},{"issue":"1\u20133","key":"9_CR15","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0168-0072(98)00039-6","volume":"96","author":"JG Henriksen","year":"1999","unstructured":"Henriksen, J.G., Thiagarajan, P.: Dynamic linear time temporal logic. Ann. Pure Appl. Logic 96(1\u20133), 187\u2013207 (1999)","journal-title":"Ann. Pure Appl. Logic"},{"key":"9_CR16","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.jlamp.2017.11.002","volume":"95","author":"E Tuosto","year":"2018","unstructured":"Tuosto, E., Guanciale, R.: Semantics of global view of choreographies. J. Logical Algebr. Methods Program. 95, 17\u201340 (2018)","journal-title":"J. Logical Algebr. Methods Program."},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. Memorandum RM-109, RAND Corporation (1951)","DOI":"10.1525\/9780520348097"},{"key":"9_CR18","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1109\/TSE.2012.64","volume":"39","author":"A Aleti","year":"2013","unstructured":"Aleti, A., Buhnova, B., Grunske, L., Koziolek, A., Meedeniya, I.: Software architecture optimization methods: a systematic literature review. IEEE Trans. Softw. Eng. 39, 658\u2013683 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9_CR19","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1016\/j.jnca.2018.03.003","volume":"110","author":"V Hayyolalam","year":"2018","unstructured":"Hayyolalam, V., Pourhaji Kazem, A.A.: A systematic literature review on QoS-aware service composition and selection in cloud environment. J. Netw. Comput. Appl. 110, 52\u201374 (2018)","journal-title":"J. Netw. Comput. Appl."},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-319-30734-3_15","volume-title":"Theory and Practice of Formal Methods","author":"E Giachino","year":"2016","unstructured":"Giachino, E., de Gouw, S., Laneve, C., Nobakht, B.: Statically and dynamically verifiable SLA metrics. In: \u00c1brah\u00e1m, E., Bonsangue, M., Johnsen, E.B. (eds.) Theory and Practice of Formal Methods. LNCS, vol. 9660, pp. 211\u2013225. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-30734-3_15"},{"key":"9_CR21","unstructured":"Rosenthal, K.: Quantales and Their Applications, vol. 234 of Pitman Research Notes in Mathematics Series. Longman Scientific & Technical (1990)"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-540-71316-6_3","volume-title":"Programming Languages and Systems","author":"MG Buscemi","year":"2007","unstructured":"Buscemi, M.G., Montanari, U.: CC-Pi: a constraint-based language for specifying service level agreements. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 18\u201332. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71316-6_3"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Lluch-Lafuente, A., Montanari, U.: Quantitative $$\\mu $$-calculus and CTL based on constraint semirings. Electron. Notes Theor. Comp. Sci. 112, 37\u201359 (2005)","DOI":"10.1016\/j.entcs.2004.02.063"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/11417019_3","volume-title":"Coordination Models and Languages","author":"R De Nicola","year":"2005","unstructured":"De Nicola, R., Ferrari, G., Montanari, U., Pugliese, R., Tuosto, E.: A process calculus for QoS-aware applications. In: Jacquet, J.-M., Picco, G.P. (eds.) COORDINATION 2005. LNCS, vol. 3454, pp. 33\u201348. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11417019_3"},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-030-22397-7_13","volume-title":"Coordination Models and Languages","author":"AE Martinez Su\u00f1\u00e9","year":"2019","unstructured":"Martinez Su\u00f1\u00e9, A.E., Lopez Pombo, C.G.: Automatic quality-of-service evaluation in service-oriented computing. In: Riis Nielson, H., Tuosto, E. (eds.) COORDINATION 2019. LNCS, vol. 11533, pp. 221\u2013236. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-22397-7_13"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-15375-4_12","volume-title":"CONCUR 2010 - Concurrency Theory","author":"L Bocchi","year":"2010","unstructured":"Bocchi, L., Honda, K., Tuosto, E., Yoshida, N.: A theory of design-by-contract for distributed multiparty interactions. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 162\u2013176. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_12"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Vissani, I., Lopez Pombo, C.G., Tuosto, E.: Communicating machines as a dynamic binding mechanism of services. In Gay, D., et al. (eds.) Proceedings of PLACES, vol. 203 of Electronics Proceedings in Theoretical Computer Science, pp. 85\u201398 (2016)","DOI":"10.4204\/EPTCS.203.7"},{"issue":"1","key":"9_CR28","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A Pnueli","year":"1981","unstructured":"Pnueli, A.: The temporal semantics of concurrent programs. Theor. Comp. Sci. 13(1), 45\u201360 (1981)","journal-title":"Theor. Comp. Sci."},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Semantical consideration on floyd-hoare logic. In Carlyle, et al. (eds.) Proceedings of 17th SFCS, pp. 109\u2013121. IEEE Computer Society (1976)","DOI":"10.1109\/SFCS.1976.27"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: The rise and fall of LTL: invited talk at the 2nd. Games, automata, logics and formal verification. Electron. Proc. Theor. Comp. Sci. 54 (2011)","DOI":"10.4204\/EPTCS.54.0.2"},{"key":"9_CR31","unstructured":"De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of 23rd IJCAI, 2013, pp. 854\u2013860. AAAI Press (2013)"},{"key":"9_CR32","unstructured":"Post Office Protocol: Version 2. RFC 937 (1985)"},{"key":"9_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"Coto, A., Guanciale, R., Tuosto, E.: Choreographic development of message-passing applications - a tutorial. In: [4], pp. 20\u201336 (2020)","DOI":"10.1007\/978-3-030-50029-0_2"},{"key":"9_CR35","unstructured":"Coto, A., Guanciale, R., Lange, J., Tuosto, E.: ChorGram: tool support for choreographic deveelopment. https:\/\/bitbucket.org\/eMgssi\/chorgram\/src\/master\/ (2015)"},{"key":"9_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-030-47361-7_6","volume-title":"Reversible Computation: Extending Horizons of Computing","author":"A Francalanza","year":"2020","unstructured":"Francalanza, A., Mezzina, C.A., Tuosto, E.: Towards choreographic-based monitoring. In: Ulidowski, I., Lanese, I., Schultz, U.P., Ferreira, C. (eds.) RC 2020. LNCS, vol. 12070, pp. 128\u2013150. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-47361-7_6"},{"key":"9_CR37","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1016\/j.tcs.2017.02.009","volume":"669","author":"L Bocchi","year":"2017","unstructured":"Bocchi, L., Chen, T., Demangeon, R., Honda, K., Yoshida, N.: Monitoring networks through multiparty session types. Theor. Comput. Sci. 669, 33\u201358 (2017)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR38","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proceedings of the International Congress on Logic, Method, and Philosophy of Science, pp. 1\u201311. Stanford University, Stanford University Press, Stanford (1962)"},{"key":"9_CR39","volume-title":"Handbook of Satisfiability","year":"2021","unstructured":"Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, 2nd edn. IOS Press, Amsterdam (2021)","edition":"2"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2023"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-47963-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,22]],"date-time":"2023-11-22T21:42:18Z","timestamp":1700689338000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-47963-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031479625","9783031479632"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-47963-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"23 November 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lima","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Peru","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 December 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 December 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ictac2023.compsust.utec.edu.pe\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}