{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T06:50:25Z","timestamp":1781938225523,"version":"3.54.5"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032283573","type":"print"},{"value":"9783032283580","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-28358-0_2","type":"book-chapter","created":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T06:01:20Z","timestamp":1781935280000},"page":"26-46","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["HistMSO: a\u00a0Logic for\u00a0Reasoning About Consistency Models with\u00a0MONA"],"prefix":"10.1007","author":[{"given":"Isabelle","family":"Coget","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8505-585X","authenticated-orcid":false,"given":"Etienne","family":"Lozes","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,21]]},"reference":[{"issue":"2","key":"2_CR1","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"2_CR2","doi-asserted-by":"publisher","unstructured":"Attiya, H., Enea, C., Rom\u00e1n-Calvo, E.: Arbitration-free consistency is available (and vice versa). CoRR abs\/2510.21304 (2025). https:\/\/doi.org\/10.48550\/ARXIV.2510.21304","DOI":"10.48550\/ARXIV.2510.21304"},{"key":"2_CR3","unstructured":"Basin, D., Klarlund, N.: Automata based symbolic reasoning in hardware verification. Formal Methods Syst. Design 13, 255\u2013288 (1998), extended version of: Hardware verification using monadic second-order logic. CAV \u201995, LNCS 939"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Bengtsson, J., Larsen, K., Larsson, F., Pettersson, P., Yi, W.: Uppaal\u2013a tool suite for automatic verification of real-time systems. In: International Hybrid Systems Workshop, pp. 232\u2013243. Springer (1995)","DOI":"10.1007\/BFb0020949"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: a model-checking tool for real-time systems. In: International Conference on Computer Aided Verification, pp. 546\u2013550. Springer (1998)","DOI":"10.1007\/BFb0028779"},{"key":"2_CR6","unstructured":"Burckhardt, S.: Principles of eventual consistency. https:\/\/www.microsoft.com\/en-us\/research\/wp-content\/uploads\/2016\/02\/final-printversion-10-5-14.pdf (2014)"},{"key":"2_CR7","doi-asserted-by":"publisher","unstructured":"Chevrou, F., Hurault, A., Nakajima, S., Qu\u00e9innec, P.: A map of asynchronous communication models. In: et al, E.S. (ed.) Formal Methods. FM 2019 International Workshops - Porto, Portugal, 7\u201311 October 2019, Revised Selected Papers, Part II. Lecture Notes in Computer Science, vol. 12233, pp. 307\u2013322. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-54997-8_20","DOI":"10.1007\/978-3-030-54997-8_20"},{"key":"2_CR8","unstructured":"Coget, I., Lozes, E.: Histmso: a logic for reasoning about consistency models with MONA (2026). https:\/\/arxiv.org\/abs\/2604.03085"},{"key":"2_CR9","unstructured":"Courcelle, B.: Special tree-width and the verification of monadic second-order graph properties. In: FSTTCS. LIPIcs, vol. 8, pp. 13\u201329. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Chennai, India (2010)"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Damgaard, N., Klarlund, N., Schwartzbach, M.I.: YakYak: parsing with logical side constraints. In: Proceedings of DLT\u201999 (1999)","DOI":"10.1142\/9789812792464_0024"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"De Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"2_CR12","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/11562948_20","volume-title":"Automated Technology for Verification and Analysis","author":"S Demri","year":"2005","unstructured":"Demri, S., Nowak, D.: Reasoning about transfinite sequences. In: Peled, D.A., Tsay, Y.K. (eds.) Automated Technology for Verification and Analysis, pp. 248\u2013262. Springer, Berlin, Heidelberg (2005)"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Di Giusto, C., Ferr\u00e9, D., Laversa, L., Lozes, \u00c9.: A partial order view of message-passing communication models. Proc. ACM Program. Lang. 7(POPL), 1601\u20131627 (2023). https:\/\/doi.org\/10.1145\/3571248","DOI":"10.1145\/3571248"},{"issue":"3","key":"2_CR14","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/S0167-6423(02)00022-9","volume":"44","author":"A Engels","year":"2002","unstructured":"Engels, A., Mauw, S., Reniers, M.: A hierarchy of communication models for message sequence charts. Sci. Comput. Program. 44(3), 253\u2013292 (2002). https:\/\/doi.org\/10.1016\/S0167-6423(02)00022-9","journal-title":"Sci. Comput. Program."},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Havelund, K., Ro\u015fu, G.: Runtime verification-17 years later. In: International Conference on Runtime Verification, pp. 3\u201317. Springer (2018)","DOI":"10.1007\/978-3-030-03769-7_1"},{"issue":"3","key":"2_CR16","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Langu. Syst. (TOPLAS) 12(3), 463\u2013492 (1990). https:\/\/doi.org\/10.1145\/78969.78972","journal-title":"ACM Trans. Program. Langu. Syst. (TOPLAS)"},{"issue":"10","key":"2_CR17","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/TSE.2007.70724","volume":"33","author":"GJ Holzmann","year":"2007","unstructured":"Holzmann, G.J., Bosnacki, D.: The design of a multicore extension of the spin model checker. IEEE Trans. Softw. Eng. 33(10), 659\u2013674 (2007)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Jensen, J.L., Joergensen, M.E., Klarlund, N., Schwartzbach, M.I.: Automatic verification of pointer programs using monadic second-order logic. In: PLDI \u201997 (1997)","DOI":"10.1145\/258915.258936"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Klarlund, N., Nielsen, M., Sunesen, K.: A case study in automated verification based on trace abstractions. In: Broy, M., Merz, S., Spies, K. (eds.) Formal System Specification, The RPC-Memory Specification Case Study. LNCS, vol. 1169, pp. 341\u2013374. Springer Verlag (1996)","DOI":"10.1007\/BFb0024435"},{"key":"2_CR20","unstructured":"Klarlund, N., M\u00f8ller, A.: Mona version 1.4 user manual (2001). https:\/\/www.brics.dk\/mona\/mona14.pdf"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and vampire. In: International Conference on Computer Aided Verification, pp. 1\u201335. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Gotsman, A., H.Y.: Understanding eventual consistency. Technical Report MSR-TR-2013-39 (2013)","DOI":"10.1561\/9781601988591"},{"key":"2_CR23","doi-asserted-by":"publisher","unstructured":"Singla, A., Ramachandran, U., Hodgins, J.K.: Temporal notions of synchronization and consistency in beehive. In: Proceedings of the Ninth Annual ACM Symposium on Parallel Algorithms and Architectures, SPAA 1997, Santa Barbara, California, USA, 23\u201325 July 1997, pp. 211\u2013220. ACM (1997). https:\/\/doi.org\/10.1145\/258492.258513","DOI":"10.1145\/258492.258513"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Viotti, P., Vukolic, M.: Consistency in non-transactional distributed storage systems. http:\/\/vukolic.com\/consistency-survey.pdf (2016)","DOI":"10.1145\/2926965"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: Spass version 3.5. In: International Conference on Automated Deduction, pp. 140\u2013145. Springer (2009)","DOI":"10.1007\/978-3-642-02959-2_10"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking tla+ specifications. In: Advanced Research Working Conference on Correct Hardware Design and Verification Methods, pp. 54\u201366. Springer (1999)","DOI":"10.1007\/3-540-48153-2_6"}],"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-032-28358-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T06:01:25Z","timestamp":1781935285000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28358-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032283573","9783032283580"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28358-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"21 June 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"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":"Urbino","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 June 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 June 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"coordination2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.discotec.org\/2026\/coordination","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}