{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T08:11:51Z","timestamp":1790842311468,"version":"4.1.0"},"reference-count":74,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T00:00:00Z","timestamp":1585872000000},"content-version":"unspecified","delay-in-days":33,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2020,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In recent times, satisfiability modulo theories (SMT) techniques gained increasing attention and obtained remarkable success in model-checking infinite-state systems. Still, we believe that whenever more expressivity is needed in order to specify the systems to be verified, more and more support is needed from mathematical logic and model theory. This is the case of the applications considered in this paper: we study verification over a general model of relational, data-aware processes, to assess (parameterized) safety properties irrespectively of the initial database (DB) instance. Toward this goal, we take inspiration from array-based systems and tackle safety algorithmically via backward reachability. To enable the adoption of this technique in our rich setting, we make use of the model-theoretic machinery of model completion, which surprisingly turns out to be an effective tool for verification of relational systems and represents the main original contribution of this paper. In this way, we pursue a twofold purpose. On the one hand, we isolate three notable classes for which backward reachability terminates, in turn witnessing decidability. Two of such classes relate our approach to conditions singled out in the literature, whereas the third one is genuinely novel. On the other hand, we are able to exploit SMT technology in implementations, building on the well-known MCMT (Model Checker Modulo Theories) model checker for array-based systems and extending it to make all our foundational results fully operational. All in all, the present contribution is deeply rooted in the long-standing tradition of the application of model theory in computer science. In particular, this paper applies these ideas in an original mathematical context and shows how these techniques can be used for the first time to empower algorithmic techniques for the verification of infinite-state systems based on arrays, so as to make such techniques applicable to the timely, challenging settings of data-aware processes.<\/jats:p>","DOI":"10.1017\/s0960129520000067","type":"journal-article","created":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T06:54:37Z","timestamp":1585896877000},"page":"271-313","source":"Crossref","is-referenced-by-count":18,"title":["SMT-based verification of data-aware processes: a model-theoretic approach"],"prefix":"10.1017","volume":"30","author":[{"given":"Diego","family":"Calvanese","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6449-6883","authenticated-orcid":false,"given":"Silvio","family":"Ghilardi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4216-5199","authenticated-orcid":false,"given":"Alessandro","family":"Gianola","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marco","family":"Montali","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrey","family":"Rivkin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2020,4,3]]},"reference":[{"key":"S0960129520000067_ref74","doi-asserted-by":"publisher","DOI":"10.1007\/BF02757007"},{"key":"S0960129520000067_ref72","article-title":"On interpolation and symbol elimination in theory extensions","volume":"14","author":"Sofronie-Stokkermans","year":"2018","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129520000067_ref70","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(4:1)2008"},{"key":"S0960129520000067_ref66","unstructured":"Robinson, A. (1963). Introduction to Model Theory and to the Metamathematics of Algebra, Studies in Logic and the Foundations of Mathematics, North-Holland."},{"key":"S0960129520000067_ref64","doi-asserted-by":"publisher","DOI":"10.4064\/aa-9-4-331-340"},{"key":"S0960129520000067_ref62","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2010-362"},{"key":"S0960129520000067_ref61","unstructured":"Nicolini, E. , Ringeissen, C. and Rusinowitch, M. (2009b). Satisfiability procedures for combination of theories sharing integer offsets. In: Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 5505, Springer, 428\u2013442."},{"key":"S0960129520000067_ref60","unstructured":"Nicolini, E. , Ringeissen, C. and Rusinowitch, M. (2009a). Data structures with arithmetic constraints: a non-disjoint combination. In: Proceedings of the 7th International Symposium on Frontiers of Combining Systems (FroCoS), LNCS (LNAI), vol. 5749, Springer, 319\u2013334."},{"key":"S0960129520000067_ref58","unstructured":"Lipparini, P. (1982). Locally finite theories with model companion. In: Atti della Accademia Nazionale dei Lincei. Classe di Scienze Fisiche, Matematiche e Naturali. Rendiconti, Serie 8, vol. 72, Accademia Nazionale dei Lincei."},{"key":"S0960129520000067_ref57","doi-asserted-by":"crossref","first-page":"283","DOI":"10.14778\/3157794.3157798","article-title":"VERIFAS: a practical verifier for artifact systems","volume":"11","author":"Li","year":"2017","journal-title":"Proceedings of the VLDB Endowment"},{"key":"S0960129520000067_ref54","unstructured":"Hull, R. (2008). Artifact-centric business process models: brief survey of research results and challenges. In: Proceedings of the OTM Confederated International Conferences, LNCS, vol. 5332, Springer, 1152\u20131163."},{"key":"S0960129520000067_ref53","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"S0960129520000067_ref52","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-2.1.326"},{"key":"S0960129520000067_ref50","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2933609"},{"key":"S0960129520000067_ref69","volume-title":"BPMN Method and Style","author":"Silver","year":"2011"},{"key":"S0960129520000067_ref49","unstructured":"Ghilardi, S. and Ranise, S. (2010b). MCMT: a model checker modulo theories. In: Proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR), LNCS (LNAI), vol. 6173, Springer, 22\u201329."},{"key":"S0960129520000067_ref48","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-6(4:10)2010"},{"key":"S0960129520000067_ref47","doi-asserted-by":"publisher","DOI":"10.1145\/1342991.1342992"},{"key":"S0960129520000067_ref45","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2018.04.001"},{"key":"S0960129520000067_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-004-6241-5"},{"key":"S0960129520000067_ref41","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782630"},{"key":"S0960129520000067_ref40","unstructured":"Dutertre, B. and De Moura, L. (2006). The YICES SMT Solver. Technical Report, SRI International."},{"key":"S0960129520000067_ref39","doi-asserted-by":"publisher","DOI":"10.1145\/3321487"},{"key":"S0960129520000067_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48168-0_5"},{"key":"S0960129520000067_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/2463664.2467796"},{"key":"S0960129520000067_ref67","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.05.007"},{"key":"S0960129520000067_ref6","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190087"},{"key":"S0960129520000067_ref13","unstructured":"Bradley, A. R. (2012). IC3 and beyond: incremental, inductive verification. In: Proceedings of the 24th International Conference on Computer Aided Verification (CAV), LNCS, vol. 7358, Springer, 4."},{"key":"S0960129520000067_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-95582-7_37"},{"key":"S0960129520000067_ref36","doi-asserted-by":"publisher","DOI":"10.1145\/3212019.3212025"},{"key":"S0960129520000067_ref21","unstructured":"Calvanese, D. , Ghilardi, S. , Gianola, A. , Montali, M. and Rivkin, A. (2019b). From model completeness to verification of data aware processes. In: Lutz, C. , Sattler, U. , Tinelli, C. , Turhan, A.-Y. , and Wolter, F. (eds.) Description Logic, Theory Combination, and All That, LNCS, vol. 11560, Springer, 212\u2013239."},{"key":"S0960129520000067_ref14","volume-title":"The Calculus of Computation - Decision Procedures with Applications to Verification","author":"Bradley","year":"2007"},{"key":"S0960129520000067_ref71","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_19"},{"key":"S0960129520000067_ref38","doi-asserted-by":"publisher","DOI":"10.1145\/2902251.2902275"},{"key":"S0960129520000067_ref68","doi-asserted-by":"crossref","unstructured":"Schmitz, S. and Schnoebelen, P. (2013). The power of well-structured systems. In: Proceedings of the 24th International Conference on Concurrency Theory (CONCUR), LNCS, vol. 8052, Springer, 5\u201324.","DOI":"10.1007\/978-3-642-40184-8_2"},{"key":"S0960129520000067_ref3","unstructured":"Alberti, F. , Bruttomesso, R. , Ghilardi, S. , Ranise, S. and Sharygina, N. (2012a). SAFARI: SMT-based abstraction for arrays with interpolants. In: Proceedings of the 24th International Conference on Computer Aided Verification (CAV), LNCS, vol. 7358, Springer, 679\u2013685."},{"key":"S0960129520000067_ref63","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"S0960129520000067_ref59","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"S0960129520000067_ref56","first-page":"251","article-title":"Nets with tokens which carry data","volume":"88","author":"Lazic","year":"2008","journal-title":"Fundamenta Informaticae"},{"key":"S0960129520000067_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_4"},{"key":"S0960129520000067_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80786-2"},{"key":"S0960129520000067_ref22","unstructured":"Calvanese, D. , Ghilardi, S. , Gianola, A. , Montali, M. and Rivkin, A. (2019c). Model completeness, covers and superposition. In: Proceedings of 27th International Conference on Automated Deduction (CADE), LNCS (LNAI), vol. 11716, Springer, 142\u2013160."},{"key":"S0960129520000067_ref27","unstructured":"Conchon, S. , Declerck, D. and Zaidi, F. (2018a). Cubicle-W: parameterized model checking on weak memory. In: Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR), LNCS (LNAI), vol. 10900, Springer, 152\u2013160."},{"key":"S0960129520000067_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15763-9_36"},{"key":"S0960129520000067_ref28","unstructured":"Conchon, S. , Delzanno, G. and Ferrando, A. (2018b). Declarative parameterized verification of topology-sensitive distributed protocols. In: Proceedings of the 6th International Conference on Networked Systems (NETYS), LNCS, vol. 11028, Springer, 209\u2013224."},{"key":"S0960129520000067_ref73","doi-asserted-by":"publisher","DOI":"10.1145\/1514894.1514896"},{"key":"S0960129520000067_ref44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66167-4_18"},{"key":"S0960129520000067_ref10","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752"},{"key":"S0960129520000067_ref18","unstructured":"Calvanese, D. , Ghilardi, S. , Gianola, A. , Montali, M. and Rivkin, A. (2018a). Quantifier Elimination for Database Driven Verification. Technical Report arXiv:1806.09686, arXiv.org."},{"key":"S0960129520000067_ref32","doi-asserted-by":"publisher","DOI":"10.1145\/2338626.2338628"},{"key":"S0960129520000067_ref23","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.311.9"},{"key":"S0960129520000067_ref1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561359"},{"key":"S0960129520000067_ref46","unstructured":"Ghilardi, S. , Nicolini, E. , Ranise, S. and Zucchelli, D. (2008a). Towards SMT model checking of array-based systems. In: Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR), LNCS (LNAI), vol. 5195, Springer, 67\u201382."},{"key":"S0960129520000067_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-014-0209-9"},{"key":"S0960129520000067_ref7","unstructured":"Alberti, F. , Ghilardi, S. and Sharygina, N. (2014b). Booster: an acceleration-based verification framework for array programs. In: Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis (ATVA), LNCS, vol. 8837, Springer, 18\u201323."},{"key":"S0960129520000067_ref8","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2017-1458"},{"key":"S0960129520000067_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.05.009"},{"key":"S0960129520000067_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/2463664.2465228"},{"key":"S0960129520000067_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"S0960129520000067_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_28"},{"key":"S0960129520000067_ref42","doi-asserted-by":"publisher","DOI":"10.1017\/S0022481200051756"},{"key":"S0960129520000067_ref19","unstructured":"Calvanese, D. , Ghilardi, S. , Gianola, A. , Montali, M. and Rivkin, A. (2018b). Verification of Data-Aware Processes via Array-Based Systems (Extended Version). Technical Report arXiv:1806.11459, arXiv.org."},{"key":"S0960129520000067_ref20","unstructured":"Calvanese, D. , Ghilardi, S. , Gianola, A. , Montali, M. and Rivkin, A. (2019a). Formal modeling and SMT-based parameterized verification of data-aware BPMN. In: Proceeding of the 17th International Conference on Business Process Management (BPM), LNCS, vol. 11675, Springer, 157\u2013175."},{"key":"S0960129520000067_ref65","volume-title":"On the Metamathematics of Algebra","author":"Robinson","year":"1951"},{"key":"S0960129520000067_ref24","unstructured":"Carioni, A. , Ghilardi, S. and Ranise, S. (2010). MCMT in the land of parametrized timed automata. In: Proceedings of the 6th International Verification Workshop (VERIFY), 47\u201364."},{"key":"S0960129520000067_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66845-1_26"},{"key":"S0960129520000067_ref25","volume-title":"Model Theory","author":"Chang","year":"1990"},{"key":"S0960129520000067_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_55"},{"key":"S0960129520000067_ref51","doi-asserted-by":"publisher","DOI":"10.1017\/jsl.2016.70"},{"key":"S0960129520000067_ref30","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679392"},{"key":"S0960129520000067_ref55","first-page":"210","article-title":"Well-quasi-ordering, the tree theorem, and Vazsonyi\u2019s conjecture","volume":"95","author":"Kruskal","year":"1960","journal-title":"Transactions of the American Mathematical Society"},{"key":"S0960129520000067_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19249-9_9"},{"key":"S0960129520000067_ref34","unstructured":"Delzanno, G. (2018). Parameterized verification of publish\/subcribe protocols via infinite-state model checking. In: Proceedings of the 33rd Italian Conference on Computational Logic (CILC), 97\u2013111."},{"key":"S0960129520000067_ref37","doi-asserted-by":"publisher","DOI":"10.1145\/1514894.1514924"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129520000067","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,13]],"date-time":"2020-04-13T09:15:09Z","timestamp":1586769309000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129520000067\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,3]]},"references-count":74,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,3]]}},"alternative-id":["S0960129520000067"],"URL":"https:\/\/doi.org\/10.1017\/s0960129520000067","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,3]]}}}