{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,17]],"date-time":"2026-06-17T13:54:08Z","timestamp":1781704448527,"version":"3.54.5"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T00:00:00Z","timestamp":1773878400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T00:00:00Z","timestamp":1773878400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100004702","name":"Universit\u00e0 degli Studi di Genova","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100004702","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2026,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    is a stateful calculus in which clauses can be activated either through interactions with the external environment or by the evaluation of time expressions. Despite the apparent simplicity of its syntax and operational model, the combination of state evolution, time reasoning, and nondeterminism gives rise to significant analytical challenges. In particular, we show that determining whether a clause is never executed is undecidable. We formally prove that this undecidability result holds even for syntactically restricted fragments: namely, the\n                    <jats:italic>time-ahead<\/jats:italic>\n                    fragment, where all time expressions are strictly positive, the\n                    <jats:italic>instantaneous<\/jats:italic>\n                    fragment, where all time expressions evaluate to zero, and the\n                    <jats:italic>determinate<\/jats:italic>\n                    fragment, where the initial states of functions and events are disjoint. On the other hand, we identify a decidable subfragment: at the intersection of the instantaneous and determinate fragments reachability becomes decidable.\n                  <\/jats:p>","DOI":"10.1007\/s10009-026-00841-5","type":"journal-article","created":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T07:48:12Z","timestamp":1773906492000},"page":"255-275","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Clause-reachability is undecidable in legal contracts"],"prefix":"10.1007","volume":"28","author":[{"given":"Giorgio","family":"Delzanno","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cosimo","family":"Laneve","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Arnaud","family":"Sangnier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gianluigi","family":"Zavattaro","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,3,19]]},"reference":[{"key":"841_CR1","volume-title":"Compilers: Principles, Techniques, and Tools","author":"A.V. 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 (2006)","edition":"2"},{"issue":"2","key":"841_CR2","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":"841_CR3","first-page":"70","volume":"9","author":"R.M. 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":"841_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139174930","volume-title":"Modern Compiler Implementation in C","author":"A.W. Appel","year":"1997","unstructured":"Appel, A.W., Ginsburg, M.: Modern Compiler Implementation in C. Cambridge University Press, Cambridge (1997)"},{"key":"841_CR5","first-page":"160","volume-title":"Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS\u201993)","author":"P.A. Abdulla","year":"1993","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\u201323, 1993, pp.\u00a0160\u2013170. IEEE Comput. Soc., Los Alamitos (1993)"},{"issue":"1","key":"841_CR6","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/S0304-3975(01)00330-9","volume":"290","author":"P.A. Abdulla","year":"2003","unstructured":"Abdulla, P.A., Jonsson, B.: Model checking of systems with many identical timed processes. Theor. Comput. Sci. 290(1), 241\u2013264 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"841_CR7","series-title":"LNCS","first-page":"53","volume-title":"ICATPN\u201901","author":"P.A. Abdulla","year":"2001","unstructured":"Abdulla, P.A., Nyl\u00e9n, A.: Timed Petri nets and bqos. In: ICATPN\u201901. LNCS, vol.\u00a02075, pp.\u00a053\u201370. Springer, Berlin (2001)"},{"key":"841_CR8","first-page":"313","volume-title":"Proc. 11th Annual IEEE Symposium on Logic in Computer Science","author":"P.A. Abdulla","year":"1996","unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: Proc. 11th Annual IEEE Symposium on Logic in Computer Science, pp.\u00a0313\u2013321. IEEE Comput. Soc., Los Alamitos (1996)"},{"key":"841_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2015.07.048","volume":"612","author":"P.A. 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."},{"issue":"1","key":"841_CR10","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1006\/inco.1996.0003","volume":"124","author":"G. C\u00e9c\u00e9","year":"1996","unstructured":"C\u00e9c\u00e9, G., Finkel, A., Purushothaman Iyer, S.: Unreliable channels are easier to verify than perfect channels. Inf. Comput. 124(1), 20\u201331 (1996)","journal-title":"Inf. Comput."},{"key":"841_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/978-3-031-08166-8_7","volume-title":"The Logic of Software. A Tasting Menu of Formal Methods - Essays Dedicated to Reiner H\u00e4hnle on the Occasion of His 60th Birthday","author":"S. Crafa","year":"2022","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. Lecture Notes in Computer Science, vol.\u00a013360, pp.\u00a0129\u2013146. Springer, Cham (2022)"},{"key":"841_CR12","doi-asserted-by":"publisher","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":"841_CR13","doi-asserted-by":"crossref","unstructured":"de Boer, F.S., Mahdi Jaghoori, 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":"841_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/978-3-031-95589-1_7","volume-title":"Coordination Models and Languages - 27th IFIP WG 6.1 International Conference, COORDINATION 2025, Held as Part of the 20th International Federated Conference on Distributed Computing Techniques, DisCoTec 2025, Proceedings","author":"G. Delzanno","year":"2025","unstructured":"Delzanno, G., Laneve, C., Sangnier, A., Zavattaro, G.: Decidability problems for micro-stipula. In: Di Giusto, C. and Ravara, A. (eds.), Coordination Models and Languages - 27th IFIP WG 6.1 International Conference, COORDINATION 2025, Held as Part of the 20th International Federated Conference on Distributed Computing Techniques, DisCoTec 2025, Proceedings, Lille, France, June 17\u201319, 2025. Lecture Notes in Computer Science, vol.\u00a015731, pp.\u00a0133\u2013152. Springer, Berlin (2025)"},{"issue":"6","key":"841_CR15","first-page":"285","volume":"19","author":"L.E. Dickson","year":"1913","unstructured":"Dickson, L.E.: Finiteness of the odd perfect and primitive abundant numbers with $n$ distinct prime factors. Bull. Am. Math. Soc. 19(6), 285 (1913)","journal-title":"Bull. Am. Math. Soc."},{"key":"841_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/BFb0055044","volume-title":"Automata, Languages and Programming, 25th International Colloquium, ICALP\u201998","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.) Automata, Languages and Programming, 25th International Colloquium, ICALP\u201998, Aalborg, Denmark, July 13\u201317, 1998. Lecture Notes in Computer Science, vol.\u00a01443, pp.\u00a0103\u2013115. Springer, Berlin (1998)"},{"issue":"3","key":"841_CR17","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":"841_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, Ph.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256, 63\u201392 (2001)","journal-title":"Theor. Comput. Sci."},{"issue":"6","key":"841_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. Electron. Notes Theor. Comput. Sci. 68(6), 85\u2013106 (2002)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1","key":"841_CR20","doi-asserted-by":"publisher","first-page":"6: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), 6:1\u20136:48 (2012)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"841_CR21","first-page":"278","volume-title":"Proceedings of the Real-Time Systems Symposium - 1990","author":"H. Hansson","year":"1990","unstructured":"Hansson, H., Jonsson, B.: A calculus for communicating systems with time and probabitilies. In: Proceedings of the Real-Time Systems Symposium - 1990, pp.\u00a0278\u2013287. IEEE Comput. Soc., New York (1990)"},{"key":"841_CR22","first-page":"339","volume-title":"Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007","author":"R. Jhala","year":"2007","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\u201319, 2007, pp.\u00a0339\u2013350. ACM, New York (2007)"},{"issue":"2","key":"841_CR23","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"R.M. 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":"841_CR24","first-page":"17:1","volume-title":"Proc. 26th International Symposium on Principles and Practice of Declarative Programming, PPDP 2024","author":"C. Laneve","year":"2024","unstructured":"Laneve, C.: Reachability analysis in micro-Stipula. In: Proc. 26th International Symposium on Principles and Practice of Declarative Programming, PPDP 2024, pp.\u00a017:1\u201317:12. ACM, New York (2024)"},{"key":"841_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"570","DOI":"10.1007\/3-540-45061-0_46","volume-title":"Automata, Languages and Programming, 30th International Colloquium, ICALP 2003. Proceedings","author":"R. Mayr","year":"2003","unstructured":"Mayr, R.: Undecidability of weak bisimulation equivalence for 1-counter processes. In: Baeten, J.C.M., Karel Lenstra, J., Parrow, J., Woeginger, G.J. (eds.) Automata, Languages and Programming, 30th International Colloquium, ICALP 2003. Proceedings, Eindhoven, The Netherlands, June 30\u2013July 4, 2003. Lecture Notes in Computer Science, vol.\u00a02719, pp.\u00a0570\u2013583. Springer, Berlin (2003)"},{"key":"841_CR26","series-title":"IFIP","first-page":"477","volume-title":"IFIP TCS","author":"R. Meyer","year":"2008","unstructured":"Meyer, R.: On boundedness in depth in the pi-calculus. In: IFIP TCS. IFIP, vol.\u00a0273, pp.\u00a0477\u2013489. Springer, Berlin (2008)"},{"key":"841_CR27","volume-title":"Computation: Finite and Infinite Machines","author":"M. Minsky","year":"1967","unstructured":"Minsky, M.: Computation: Finite and Infinite Machines. Prentice Hall, New York (1967)"},{"key":"841_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/BFb0039073","volume-title":"Proceedings of CONCUR\u201990","author":"F. Moller","year":"1990","unstructured":"Moller, F., Tofts, C.M.N.: A temporal calculus of communicating systems. In: Proceedings of CONCUR\u201990. Lecture Notes in Computer Science, vol.\u00a0458, pp.\u00a0401\u2013415. Springer, Berlin (1990)"},{"key":"841_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"300","DOI":"10.1007\/11817963_29","volume-title":"Computer Aided Verification, 18th International Conference, CAV 2006, Proceedings","author":"K. Sen","year":"2006","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, Proceedings Seattle, WA, USA, August 17\u201320, 2006. Lecture Notes in Computer Science, vol.\u00a04144, pp.\u00a0300\u2013314. Springer, Berlin (2006)"},{"key":"841_CR30","unstructured":"Stipula Reachability Analyzer, S.E.: (2024). Available on github. https:\/\/github.com\/stipula-language"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-026-00841-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-026-00841-5","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-026-00841-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,17]],"date-time":"2026-06-17T13:05:49Z","timestamp":1781701549000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-026-00841-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,3,19]]},"references-count":30,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2026,6]]}},"alternative-id":["841"],"URL":"https:\/\/doi.org\/10.1007\/s10009-026-00841-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,3,19]]},"assertion":[{"value":"20 February 2026","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 March 2026","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}