{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T09:24:07Z","timestamp":1743153847312,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031626968"},{"type":"electronic","value":"9783031626975"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-62697-5_2","type":"book-chapter","created":{"date-parts":[[2024,6,10]],"date-time":"2024-06-10T21:01:23Z","timestamp":1718053283000},"page":"20-37","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Probabilistic Choreography Language for\u00a0PRISM"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9479-2632","authenticated-orcid":false,"given":"Marco","family":"Carbone","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0403-1889","authenticated-orcid":false,"given":"Adele","family":"Veschetti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,6,11]]},"reference":[{"unstructured":"ANTLR - another tool for language recognition. https:\/\/www.antlr.org\/","key":"2_CR1"},{"unstructured":"Prism documentation. https:\/\/www.prismmodelchecker.org\/. Accessed 05 Sep 2023","key":"2_CR2"},{"unstructured":"Repository. https:\/\/github.com\/adeleveschetti\/ChoreoPRISM, Accessed 31 Jan 2024","key":"2_CR3"},{"doi-asserted-by":"publisher","unstructured":"Aman, B., Ciobanu, G.: Probabilities in session types. In: Marin, M., Craciun, A. (eds.) Proceedings Third Symposium on Working Formal Methods, FROM 2019, Timi\u015foara, Romania, 3\u20135 September 2019. EPTCS, vol.\u00a0303, pp. 92\u2013106 (2019). https:\/\/doi.org\/10.4204\/EPTCS.303.7","key":"2_CR4","DOI":"10.4204\/EPTCS.303.7"},{"doi-asserted-by":"publisher","unstructured":"Aman, B., Ciobanu, G.: Interval probability for sessions types. In: Ciabattoni, A., Pimentel, E., de\u00a0Queiroz, R.J.G.B. (eds.) Logic, Language, Information, and Computation - 28th International Workshop, WoLLIC 2022, Ia\u015fi, Romania, September 20-23, 2022, Proceedings. LNCS, vol. 13468, pp. 123\u2013140. Springer, Cham (2022).https:\/\/doi.org\/10.1007\/978-3-031-15298-6_8","key":"2_CR5","DOI":"10.1007\/978-3-031-15298-6_8"},{"doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., Massink, M., Latella, D., Gnesi, S., Forghieri, A., Sebastianis, M.: Model checking publish\/subscribe notification for thinkteam\u00ae. In: FMICS. Electronic Notes in Theoretical Computer Science, vol.\u00a0133, pp. 275\u2013294. Elsevier (2004)","key":"2_CR6","DOI":"10.1016\/j.entcs.2004.08.069"},{"doi-asserted-by":"publisher","unstructured":"Bistarelli, S., Nicola, R.D., Galletta, L., Laneve, C., Mercanti, I., Veschetti, A.: Stochastic modeling and analysis of the bitcoin protocol in the presence of block communication delays. Concurr. Comput. Pract. Exp. 35(16) (2023). https:\/\/doi.org\/10.1002\/cpe.6749","key":"2_CR7","DOI":"10.1002\/cpe.6749"},{"doi-asserted-by":"publisher","unstructured":"Carbone, M., Grohmann, D., Hildebrandt, T.T., L\u00f3pez, H.A.: A logic for choreographies. In: Honda, K., Mycroft, A. (eds.) Proceedings Third Workshop on Programming Language Approaches to Concurrency and communication-cEntric Software, PLACES 2010, Paphos, Cyprus, 21st March 2010. EPTCS, vol.\u00a069, pp. 29\u201343 (2010).https:\/\/doi.org\/10.4204\/EPTCS.69.3","key":"2_CR8","DOI":"10.4204\/EPTCS.69.3"},{"doi-asserted-by":"publisher","unstructured":"Carbone, M., Honda, K., Yoshida, N.: Structured communication-centered programming for web services. ACM Trans. Program. Lang. Syst. 34(2), 8:1\u20138:78 (2012). https:\/\/doi.org\/10.1145\/2220365.2220367","key":"2_CR9","DOI":"10.1145\/2220365.2220367"},{"doi-asserted-by":"publisher","unstructured":"Carbone, M., Montesi, F.: Deadlock-freedom-by-design: multiparty asynchronous global programming. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Rome, Italy - January 23\u201325, 2013, pp. 263\u2013274. ACM (2013). https:\/\/doi.org\/10.1145\/2429069.2429101","key":"2_CR10","DOI":"10.1145\/2429069.2429101"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-319-01928-4_3","volume-title":"DNA Computing and Molecular Programming","author":"F Dannenberg","year":"2013","unstructured":"Dannenberg, F., Kwiatkowska, M., Thachuk, C., Turberfield, A.J.: DNA walker circuits: computational potential, design, and verification. In: Soloveichik, D., Yurke, B. (eds.) DNA 2013. LNCS, vol. 8141, pp. 31\u201345. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-01928-4_3"},{"doi-asserted-by":"publisher","unstructured":"Galletta, L., Laneve, C., Mercanti, I., Veschetti, A.: Resilience of hybrid casper under varying values of parameters. Distributed Ledger Technol. Res. Pract. 2(1), 5:1\u20135:25 (2023).https:\/\/doi.org\/10.1145\/3571587","key":"2_CR12","DOI":"10.1145\/3571587"},{"doi-asserted-by":"publisher","unstructured":"Giallorenzo, S., Montesi, F., Peressotti, M.: Choral: Object-oriented choreographic programming. ACM Trans. Program. Lang. Syst. 46(1), 1:1\u20131:59 (2024). https:\/\/doi.org\/10.1145\/3632398","key":"2_CR13","DOI":"10.1145\/3632398"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/11885191_3","volume-title":"Computational Methods in Systems Biology","author":"J Heath","year":"2006","unstructured":"Heath, J., Kwiatkowska, M., Norman, G., Parker, D., Tymchyshyn, O.: Probabilistic model checking of complex biological pathways. In: Priami, C. (ed.) CMSB 2006. LNCS, vol. 4210, pp. 32\u201347. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11885191_3"},{"key":"2_CR15","first-page":"160","volume":"91","author":"K Honda","year":"2007","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Web services, mobile processes and types. Bull. EATCS 91, 160\u2013185 (2007)","journal-title":"Bull. EATCS"},{"issue":"4","key":"2_CR16","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/s00165-012-0227-6","volume":"24","author":"M Kwiatkowska","year":"2012","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic verification of hermans self-stabilisation algorithm. Formal Aspects Comput. 24(4), 661\u2013670 (2012)","journal-title":"Formal Aspects Comput."},{"issue":"12\u201313","key":"2_CR17","doi-asserted-by":"publisher","first-page":"1272","DOI":"10.1016\/j.tcs.2008.12.058","volume":"410","author":"M Kwiatkowska","year":"2009","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Vigliotti, M.: Probabilistic mobile ambients. Theoret. Comput. Sci. 410(12\u201313), 1272\u20131303 (2009)","journal-title":"Theoret. Comput. Sci."},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/3-540-44585-4_17","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2001","unstructured":"Kwiatkowska, M., Norman, G., Segala, R.: Automated verification of a randomized distributed consensus protocol using cadence SMV and PRISM? In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 194\u2013206. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_17"},{"issue":"3","key":"2_CR19","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/s001650300007","volume":"14","author":"M Kwiatkowska","year":"2003","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Formal Aspects Comput. 14(3), 295\u2013318 (2003)","journal-title":"Formal Aspects Comput."},{"doi-asserted-by":"crossref","unstructured":"Montesi, F.: Introduction to Choreographies. Cambridge University Press, Cambridge (2023)","key":"2_CR20","DOI":"10.1017\/9781108981491"},{"unstructured":"Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008). https:\/\/bitcoin.org\/bitcoin.pdf","key":"2_CR21"},{"issue":"6","key":"2_CR22","doi-asserted-by":"publisher","first-page":"561","DOI":"10.3233\/JCS-2006-14604","volume":"14","author":"G Norman","year":"2006","unstructured":"Norman, G., Shmatikov, V.: Analysis of probabilistic contract signing. J. Comput. Secur. 14(6), 561\u2013589 (2006)","journal-title":"J. Comput. Secur."}],"container-title":["Lecture Notes in Computer Science","Coordination Models and Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-62697-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,10]],"date-time":"2024-06-10T21:01:45Z","timestamp":1718053305000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-62697-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031626968","9783031626975"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-62697-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"11 June 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"COORDINATION","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Coordination Models and Languages","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Groningen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"The Netherlands","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"coordination2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}