{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,7]],"date-time":"2026-05-07T15:16:25Z","timestamp":1778166985289,"version":"3.51.4"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031955884","type":"print"},{"value":"9783031955891","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-95589-1_7","type":"book-chapter","created":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T14:48:32Z","timestamp":1750171712000},"page":"133-152","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Decidability Problems for\u00a0Micro-Stipula"],"prefix":"10.1007","author":[{"given":"G.","family":"Delzanno","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C.","family":"Laneve","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Sangnier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.","family":"Zavattaro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,6,18]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A.,\u00a0Nyl\u00e9n, A.: Timed petri nets and bqos. In: ICATPN\u201901, LNCS, vol. 2075, pp. 53\u201370. Springer (2001)","DOI":"10.1007\/3-540-45740-2_5"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.K.: General decidability theorems for infinite-state systems. In: Proceedings of the11th Annual IEEE Symposium on Logic in Computer Science, pp. 313\u2013321. IEEE Computer Society (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"7_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2015.07.048","volume":"612","author":"PA Abdulla","year":"2016","unstructured":"Abdulla, P.A., Delzanno, G., Rezine, O., Sangnier, A., Traverso, R.: Parameterized verification of time-sensitive models of ad HOC network protocols. Theor. Comput. Sci. 612, 1\u201322 (2016)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. In: Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS \u201993), Montreal, Canada, June 19-23, 1993, pp. 160\u2013170. IEEE Computer Society (1993)","DOI":"10.1109\/LICS.1993.287591"},{"issue":"1","key":"7_CR5","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/S0304-3975(01)00330-9","volume":"290","author":"PA Abdulla","year":"2003","unstructured":"Abdulla, P.A., Jonsson, B.: Model checking of systems with many identical timed processes. TCS 290(1), 241\u2013264 (2003)","journal-title":"TCS"},{"key":"7_CR6","volume-title":"Compilers: Principles, Techniques, and Tools","author":"AV Aho","year":"2006","unstructured":"Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools, 2nd edn. Addison Wesley, Boston, MA, USA (2006)","edition":"2"},{"issue":"2","key":"7_CR7","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. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"7_CR8","first-page":"70","volume":"9","author":"RM Amadio","year":"2002","unstructured":"Amadio, R.M., Meyssonnier, C.: On decidability of the control reachability problem in the asynchronous pi-calculus. Nord. J. Comput. 9(2), 70\u2013101 (2002)","journal-title":"Nord. J. Comput."},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Appel, A.W., Ginsburg, M.: Modern Compiler Implementation in C. Cambridge University Press, Cambridge, UK (1997)","DOI":"10.1017\/CBO9781139174930"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"C\u00e9c\u00e9, G., Finkel, A., Iyer, S.P.: Unreliable channels are easier to verify than perfect channels. Inf. Comput. 124(1), 20\u201331 (1996)","DOI":"10.1006\/inco.1996.0003"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Crafa, S., Laneve, C.: Programming legal contracts - a beginners guide to Stipula. In: The Logic of Software. A Tasting Menu of Formal Methods - Essays Dedicated to Reiner H\u00e4hnle on the Occasion of His 60th Birthday, volume 13360 of Lecture Notes in Computer Science, pp. 129\u2013146. Springer, Cham (2022)","DOI":"10.1007\/978-3-031-08166-8_7"},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"102911","DOI":"10.1016\/j.scico.2022.102911","volume":"225","author":"S Crafa","year":"2023","unstructured":"Crafa, S., Laneve, C., Sartor, G., Veschetti, A.: Pacta sunt servanda: legal contracts in Stipula. Sci. Comput. Program. 225, 102911 (2023)","journal-title":"Sci. Comput. Program."},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"De Boer, F. S., Jaghoori, M.M., Laneve, C., Zavattaro, G.: Decidability problems for actor systems. Log. Methods Comput. Sci. 10(4) (2014)","DOI":"10.2168\/LMCS-10(4:5)2014"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Delzanno, G., Laneve, C., Sangnier, A., Zavattaro, G.: Decidability problems for micro-Stipula (2025.) arXiv:2504.16703","DOI":"10.1007\/978-3-031-95589-1_7"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/BFb0055044","volume-title":"Automata, Languages and Programming","author":"C Dufourd","year":"1998","unstructured":"Dufourd, C., Finkel, A., Schnoebelen, P.: Reset nets between decidability and undecidability. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 103\u2013115. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055044"},{"issue":"3","key":"7_CR16","first-page":"143","volume":"30","author":"J Esparza","year":"1994","unstructured":"Esparza, J., Nielsen, M.: Decidability issues for petri nets - a survey. J. Inf. Process. Cybern. 30(3), 143\u2013160 (1994)","journal-title":"J. Inf. Process. Cybern."},{"key":"7_CR17","unstructured":"Evangelisti, S.: Stipula reachability analyzer (2024). Available on github: https:\/\/github.com\/stipula-language"},{"key":"7_CR18","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256, 63\u201392 (2001)","journal-title":"Theor. Comput. Sci."},{"issue":"6","key":"7_CR19","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S1571-0661(04)80535-8","volume":"68","author":"A Finkel","year":"2002","unstructured":"Finkel, A., Raskin, J.-F., Samuelides, M., Van Begin, L.: Monotonic extensions of petri nets: forward and backward search revisited. Electr. Notes Theor. Comput. Sci. 68(6), 85\u2013106 (2002)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1","key":"7_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2160910.2160915","volume":"34","author":"P Ganty","year":"2012","unstructured":"Ganty, P., Majumdar, R.: Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst. 34(1), 1\u201348 (2012)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Hansson, H., Jonsson, B.: A calculus for communicating systems with time and probabitilies. In: Proceedings of the Real-Time Systems Symposium - 1990, pp. 278\u2013287. IEEE Computer Society, New York (1990)","DOI":"10.1109\/REAL.1990.128759"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Jhala, R., Majumdar, R.: Interprocedural analysis of asynchronous programs. In: Hofmann, M., Felleisen, M., (eds.) Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pp. 339\u2013350. ACM (2007)","DOI":"10.1145\/1190216.1190266"},{"issue":"2","key":"7_CR23","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"RM Karp","year":"1969","unstructured":"Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147\u2013195 (1969)","journal-title":"J. Comput. Syst. Sci."},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Laneve, C.: Reachability analysis in micro-Stipula. In: Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming, PPDP 2024, pp. 1\u201312. ACM (2024)","DOI":"10.1145\/3678232.3678247"},{"key":"7_CR25","unstructured":"Mayr, R.: Undecidability of weak bisimulation equivalence for 1-counter processes. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J., (eds.) Automata, Languages and Programming, 30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands, June 30 - July 4, 2003. Proceedings, volume 2719 of Lecture Notes in Computer Science, pp. 570\u2013583. Springer (2003)"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Meyer, R.: On boundedness in depth in the pi-calculus. In: IFIP TCS, volume 273 of IFIP, pp. 477\u2013489. Springer (2008)","DOI":"10.1007\/978-0-387-09680-3_32"},{"key":"7_CR27","unstructured":"Minsky, M.: Computation: Finite and Infinite Machines. Prentice Hall (1967)"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/BFb0039073","volume-title":"CONCUR \u201990 Theories of Concurrency: Unification and Extension","author":"F Moller","year":"1990","unstructured":"Moller, F., Tofts, C.: A temporal calculus of communicating systems. In: Baeten, J., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 401\u2013415. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0039073"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M.: Model checking multithreaded programs with asynchronous atomic methods. In: Ball, T., Jones, R.B., (eds.) Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4144 of Lecture Notes in Computer Science, pp. 300\u2013314. Springer (2006)","DOI":"10.1007\/11817963_29"}],"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-95589-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,7]],"date-time":"2026-05-07T14:53:06Z","timestamp":1778165586000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-95589-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031955884","9783031955891"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-95589-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"18 June 2025","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":"Lille","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 June 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 June 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"coordination2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.discotec.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}