{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T02:42:34Z","timestamp":1768272154638,"version":"3.49.0"},"reference-count":109,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T00:00:00Z","timestamp":1745884800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T00:00:00Z","timestamp":1745884800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100021856","name":"Ministero dell\u2019Universit\u00e0 e della Ricerca","doi-asserted-by":"publisher","award":["B87G22000450001"],"award-info":[{"award-number":["B87G22000450001"]}],"id":[{"id":"10.13039\/501100021856","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100008815","name":"Libera Universit\u00e0 di Bolzano","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100008815","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["K\u00fcnstl Intell"],"published-print":{"date-parts":[[2025,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Process mining is witnessing a shift from pure control-flow process models to richer, data-aware process models where the acceptable executions are not only characterised by the process control-flow, but also by the data carried by cases, and how they dynamically interact with the process activities and decisions. Even under the typical assumption that the process control-flow is bounded, the presence of data makes the overall state space infinite, a difficulty that transfers to process analysis and process mining tasks. In this article, we review how the challenges posed by data-aware process mining can be effectively tackled through AI techniques grounded in automated reasoning, and more specifically in Satisfiability and Optimisation Modulo Theories (SMT\/OMT). To this end, we discuss data-aware logs and traces merging events with a payload. We then recall Data Petri Nets as an expressive process modelling approach matching this multi-perspective setting, and the logic <jats:inline-formula>\n              <jats:alternatives>\n                <jats:tex-math>$$\\textsf {data-}{\\textsf {LTL}_f}$$<\/jats:tex-math>\n                <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>data<\/mml:mi>\n                    <mml:mo>-<\/mml:mo>\n                    <mml:msub>\n                      <mml:mi>LTL<\/mml:mi>\n                      <mml:mi>f<\/mml:mi>\n                    <\/mml:msub>\n                  <\/mml:mrow>\n                <\/mml:math>\n              <\/jats:alternatives>\n            <\/jats:inline-formula> to formulate correctness properties and to represent declarative process constraints enriched with data. We then summarize how key process analysis and mining tasks can be addressed in this setting using SMT and OMT, with a particular focus on correctness and conformance checking, model repair, and monitoring. We overview the obtained results, presenting them under an integrated lens and providing corresponding pointers to the technical literature. In the conclusion, we outlook open challenges.<\/jats:p>","DOI":"10.1007\/s13218-025-00890-z","type":"journal-article","created":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T08:26:47Z","timestamp":1745915207000},"page":"221-237","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["SMT Techniques for Data-Aware Process Mining"],"prefix":"10.1007","volume":"39","author":[{"given":"Alessandro","family":"Gianola","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8021-3430","authenticated-orcid":false,"given":"Marco","family":"Montali","sequence":"additional","affiliation":[]},{"given":"Sarah","family":"Winkler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,4,29]]},"reference":[{"key":"890_CR1","unstructured":"cvc5. https:\/\/github.com\/cvc5\/cvc5"},{"key":"890_CR2","unstructured":"IEEE 1849-2016 XES Standard. https:\/\/xes-standard.org"},{"key":"890_CR3","unstructured":"MathSAT5. https:\/\/mathsat.fbk.eu\/"},{"key":"890_CR4","unstructured":"The Yices SMT Solver. https:\/\/yices.csl.sri.com\/"},{"key":"890_CR5","doi-asserted-by":"crossref","unstructured":"van\u00a0der Aalst WMP (2016) Process mining: data science in action. Springer","DOI":"10.1007\/978-3-662-49851-4"},{"key":"890_CR6","doi-asserted-by":"crossref","unstructured":"van\u00a0der Aalst WMP (2022) Process mining: a 360 degree overview. In: van\u00a0der Aalst WMP, Carmona J (eds) Process mining handbook. Lecture notes in business information processing, vol. 448. Springer, pp 3\u201334","DOI":"10.1007\/978-3-031-08848-3_1"},{"key":"890_CR7","unstructured":"van\u00a0der Aalst WMP (2023) Twin transitions powered by event data - using object-centric process mining to make processes digital and sustainable. In: Gomes L, Leit\u00e3o P, Lorenz R, van\u00a0der Werf JMEM, van Zelst SJ (eds.) Joint proceedings of the workshop on algorithms & theories for the analysis of event data and the international workshop on petri nets for twin transition. CEUR workshop proceedings, vol. 3424. CEUR-WS.org"},{"issue":"1\u20134","key":"890_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3233\/FI-2020-1946","volume":"175","author":"WMP van der Aalst","year":"2020","unstructured":"van der Aalst WMP, Berti A (2020) Discovering object-centric petri nets. Fundam Informaticae 175(1\u20134):1\u201340","journal-title":"Fundam Informaticae"},{"issue":"3","key":"890_CR9","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/s00165-010-0161-4","volume":"23","author":"WMP van der Aalst","year":"2011","unstructured":"van der Aalst WMP, van Hee KM, ter Hofstede AHM, Sidorova N, Verbeek HMW, Voorhoeve M, Wynn MT (2011) Soundness of workflow nets: classification, decidability, and analysis. Formal Aspects Comput 23(3):333\u2013363","journal-title":"Formal Aspects Comput"},{"key":"890_CR10","unstructured":"Adriansyah A (2014) Aligning observed and modeled behavior. Ph.D. thesis, Technische Universiteit Eindhoven"},{"key":"890_CR11","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2023.102271","volume":"119","author":"A Alman","year":"2023","unstructured":"Alman A, Maggi FM, Montali M, Patrizi F, Rivkin A (2023) A framework for modeling, executing, and monitoring hybrid multi-process specifications with bounded global-local memory. Inf Syst 119:102271","journal-title":"Inf Syst"},{"key":"890_CR12","doi-asserted-by":"crossref","unstructured":"Artale A, Kovtunova A, Montali M, van\u00a0der Aalst WMP (2019) Modeling and reasoning over declarative data-aware processes with object-centric behavioral constraints. In: Hildebrandt TT, van Dongen BF, R\u00f6glinger M, Mendling J (eds.) Proceedings of the 17th international conference on business process management (BPM 2019). Lecture notes in computer science, vol. 11675, Springer, pp 139\u2013156","DOI":"10.1007\/978-3-030-26619-6_11"},{"issue":"2","key":"890_CR13","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1145\/3651161","volume":"25","author":"A Artale","year":"2024","unstructured":"Artale A, Mazzullo A, Ozaki A (2024) First-order temporal logic on finite traces: semantic properties, decidable fragments, and applications. ACM Trans Comput Log 25(2):131\u20131343","journal-title":"ACM Trans Comput Log"},{"key":"890_CR14","doi-asserted-by":"crossref","unstructured":"Bagheri\u00a0Hariri B, Calvanese D, De\u00a0Giacomo G, Deutsch A, Montali M (2013) Verification of relational data-centric dynamic systems with external services. In: Proceedings of PODS 2013, pp 163\u2013174","DOI":"10.1145\/2463664.2465221"},{"key":"890_CR15","unstructured":"Baier C, Katoen J (2008) Principles of model checking. MIT Press"},{"key":"890_CR16","doi-asserted-by":"crossref","unstructured":"Baral C, Giacomo GD (2015) Knowledge representation and reasoning: what\u2019s hot. In: Bonet B, Koenig S (eds.) Proceedings of the twenty-ninth AAAI conference on artificial intelligence (AAAI 2015), AAAI Press , pp 4316\u20134317","DOI":"10.1609\/aaai.v29i1.9344"},{"key":"890_CR17","doi-asserted-by":"crossref","unstructured":"Barbosa H, Barrett CW, Brain M, Kremer G, Lachnitt H, Mann M, Mohamed A, Mohamed M, Niemetz A, N\u00f6tzli A, Ozdemir A, Preiner M, Reynolds A, Sheng Y, Tinelli C, Zohar Y (2022) cvc5: a versatile and industrial-strength SMT solver. In: Fisman D, Rosu G (eds) Proceedings of the 28th international conference on tools and algorithms for the construction and analysis of systems (TACAS 2022). Lecture notes in computer science, vol. 13243. Springer , pp 415\u2013442","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"890_CR18","unstructured":"Barrett C, Fontaine P, Tinelli C (2018) The SMT-LIB standard: version 2.6. Technical report, Available at: http:\/\/smtlib.cs.uiowa.edu\/language.shtml"},{"key":"890_CR19","doi-asserted-by":"crossref","unstructured":"Barrett CW, Sebastiani R, Seshia SA, Tinelli C (2021) Satisfiability modulo theories. In: Biere A, Heule M, van Maaren H, Walsh T (eds.) Handbook of satisfiability - Second Edition. Frontiers in artificial intelligence and applications, vol. 336. IOS Press, pp 1267\u20131329","DOI":"10.3233\/FAIA201017"},{"key":"890_CR20","doi-asserted-by":"crossref","unstructured":"Barrett CW, Tinelli C (2018) Satisfiability modulo theories. In: Handbook of model checking, pp. 305\u2013343","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"890_CR21","doi-asserted-by":"crossref","unstructured":"Batoulis K, Haarmann S, Weske M (2017) Various notions of soundness for decision-aware business processes. In: Mayr HC, Guizzardi G, Ma H, Pastor O (eds) Proceedings of the 36th international conference on conceptual modeling (ER 2017). Lecture notes in computer science, vol. 10650. Springer, pp 403\u2013418","DOI":"10.1007\/978-3-319-69904-2_31"},{"issue":"4","key":"890_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer A, Leucker M, Schallhart C (2011) Runtime verification for LTL and TLTL. ACM Trans Softw Eng Methodol 20(4):1\u201364. https:\/\/doi.org\/10.1145\/2000799.2000800","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"890_CR23","doi-asserted-by":"crossref","unstructured":"Bergami G, Maggi FM, Marrella A, Montali M (2021) Aligning data-aware declarative process models and event logs. In: Polyvyanyy A, Wynn MT, Van\u00a0Looy A, Reichert M (eds) Proceedings of the 19th international conference on business process management (BPM 2021). Lecture notes in computer science, vol. 12875. Springer , pp. 235\u2013251","DOI":"10.1007\/978-3-030-85469-0_16"},{"key":"890_CR24","doi-asserted-by":"publisher","unstructured":"Berti A, Montali M, van\u00a0der Aalst WMP (2023) Advancements and challenges in object-centric process mining: a systematic literature review. CoRR abs\/2311.08795 https:\/\/doi.org\/10.48550\/ARXIV.2311.08795","DOI":"10.48550\/ARXIV.2311.08795"},{"key":"890_CR25","doi-asserted-by":"crossref","unstructured":"Besold TR, d\u2019Avila Garcez AS, Bader S, Bowman H, Domingos PM, Hitzler P, K\u00fchnberger K, Lamb LC, Lima PMV, de\u00a0Penning L, Pinkas G, Poon H, Zaverucha G (2021) Neural-symbolic learning and reasoning: a survey and interpretation. In: Hitzler P, Sarker MK (eds) Neuro-symbolic artificial intelligence: the state of the art. Frontiers in artificial intelligence and applications, vol. 342. IOS Press, pp. 1\u201351","DOI":"10.3233\/FAIA210348"},{"key":"890_CR26","doi-asserted-by":"publisher","unstructured":"Boltenhagen M, Chatain T, Carmona J (2019) Encoding conformance checking artefacts in SAT. In: Proc. business process management workshops 2019, LNCS, vol. 362, pp 160\u2013171 https:\/\/doi.org\/10.1007\/978-3-030-37453-2_14","DOI":"10.1007\/978-3-030-37453-2_14"},{"issue":"1","key":"890_CR27","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/S00607-020-00831-8","volume":"103","author":"M Boltenhagen","year":"2021","unstructured":"Boltenhagen M, Chatain T, Carmona J (2021) Optimized SAT encoding of conformance checking artefacts. Computing 103(1):29\u201350. https:\/\/doi.org\/10.1007\/S00607-020-00831-8","journal-title":"Computing"},{"issue":"2","key":"890_CR28","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/j.is.2011.08.003","volume":"37","author":"RPJC Bose","year":"2012","unstructured":"Bose RPJC, van der Aalst WMP (2012) Process diagnostics using trace alignment: opportunities, issues, and challenges. Inf Syst 37(2):117\u2013141","journal-title":"Inf Syst"},{"key":"890_CR29","doi-asserted-by":"publisher","unstructured":"Buliga A, Di\u00a0Francescomarino C, Ghidini C, Donadello I, Maggi FM (2024) Guiding the generation of counterfactual explanations through temporal background knowledge for predictive process monitoring. CoRR abs\/2403.11642 https:\/\/doi.org\/10.48550\/ARXIV.2403.11642","DOI":"10.48550\/ARXIV.2403.11642"},{"key":"890_CR30","doi-asserted-by":"crossref","unstructured":"Buliga A, Di\u00a0Francescomarino C, Ghidini C, Montali M, Ronzani M (2025) Generating counterfactual explanations under temporal constraints. In: Proceedings of the 39th AAAI conference on artificial intelligence (AAAI 2025). AAAI Press. To appear","DOI":"10.1609\/aaai.v39i15.33715"},{"key":"890_CR31","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/j.eswa.2016.08.040","volume":"65","author":"A Burattin","year":"2016","unstructured":"Burattin A, Maggi FM, Sperduti A (2016) Conformance checking based on multi-perspective declarative process models. Expert Syst Appl 65:194\u2013211","journal-title":"Expert Syst Appl"},{"key":"890_CR32","doi-asserted-by":"crossref","unstructured":"Calvanese D, de Giacomo G, Montali M (2013) Foundations of data-aware process analysis: a database theory perspective. In: Proc. 32nd PODS, pp. 1\u201312","DOI":"10.1145\/2463664.2467796"},{"key":"890_CR33","unstructured":"Calvanese D, Ghilardi S, Gianola A, Montali M, Rivkin A (2018) Verification of data-aware processes via array-based systems (extended version). CoRR abs\/1806.11459. http:\/\/arxiv.org\/abs\/1806.11459"},{"key":"890_CR34","doi-asserted-by":"crossref","unstructured":"Calvanese D, Ghilardi S, Gianola A, Montali M, Rivkin A (2019) Formal modeling and SMT-based parameterized verification of data-aware BPMN. In: Proceeding of BPM 2019. LNCS, vol. 11675. Springer, pp 157\u2013175","DOI":"10.1007\/978-3-030-26619-6_12"},{"key":"890_CR35","doi-asserted-by":"crossref","unstructured":"Calvanese D, Ghilardi S, Gianola A, Montali M, Rivkin A (2019) Verification of data-aware processes: challenges and opportunities for automated reasoning. In: Proceedings of ARCADE 2019, vol. 311. EPTCS","DOI":"10.4204\/EPTCS.311.9"},{"issue":"3","key":"890_CR36","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1017\/S0960129520000067","volume":"30","author":"D Calvanese","year":"2020","unstructured":"Calvanese D, Ghilardi S, Gianola A, Montali M, Rivkin A (2020) SMT-based verification of data-aware processes: a model-theoretic approach. Math Struct Comput Sci 30(3):271\u2013313. https:\/\/doi.org\/10.1017\/S0960129520000067","journal-title":"Math Struct Comput Sci"},{"issue":"7","key":"890_CR37","doi-asserted-by":"publisher","first-page":"941","DOI":"10.1007\/S10817-021-09596-X","volume":"65","author":"D Calvanese","year":"2021","unstructured":"Calvanese D, Ghilardi S, Gianola A, Montali M, Rivkin A (2021) Model completeness, uniform interpolants and superposition calculus (with applications to verificaton of data-aware processes). J Autom Reason 65(7):941\u2013969. https:\/\/doi.org\/10.1007\/S10817-021-09596-X","journal-title":"J Autom Reason"},{"key":"890_CR38","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-022-09627-1","author":"D Calvanese","year":"2022","unstructured":"Calvanese D, Ghilardi S, Gianola A, Montali M, Rivkin A (2022) Combination of uniform interpolants via beth definability. J Autom Reason. https:\/\/doi.org\/10.1007\/S10817-022-09627-1","journal-title":"J Autom Reason"},{"key":"890_CR39","doi-asserted-by":"crossref","unstructured":"Calvanese D, Giacomo GD, Montali M, Patrizi F (2022) Verification and monitoring for first-order LTL with persistence-preserving quantification over finite and infinite traces. In: Raedt LD (ed.) Proceedings of the 31st international joint conference on artificial intelligence (IJCAI 2022), pp. 2553\u20132560. ijcai.org","DOI":"10.24963\/ijcai.2022\/354"},{"key":"890_CR40","doi-asserted-by":"publisher","unstructured":"Chatain T, Carmona J (2016) Anti-alignments in conformance checking \u2013 the dark side of process models. In: Proc. 37th Petri Nets, LNCS, vol. 9698, pp. 240\u2013258. https:\/\/doi.org\/10.1007\/978-3-319-39086-4_15","DOI":"10.1007\/978-3-319-39086-4_15"},{"key":"890_CR41","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1016\/j.is.2016.09.005","volume":"64","author":"CD Ciccio","year":"2017","unstructured":"Ciccio CD, Maggi FM, Montali M, Mendling J (2017) Resolving inconsistencies and redundancies in declarative process models. Inf Syst 64:425\u2013446","journal-title":"Inf Syst"},{"key":"890_CR42","doi-asserted-by":"crossref","unstructured":"Ciccio CD, Montali M (2022) Declarative process specifications: reasoning, discovery, monitoring. In: van\u00a0der Aalst WMP, Carmona J (eds) Process mining handbook. Lecture notes in business information processing, vol. 448. Springer, pp. 108\u2013152","DOI":"10.1007\/978-3-031-08848-3_4"},{"key":"890_CR43","doi-asserted-by":"crossref","unstructured":"Cimatti A, Griggio A, Schaafsma BJ, Sebastiani R (2013) The mathsat5 SMT solver. In: Proceedings of TACAS 2013. LNCS, vol. 7795. Springer, pp. 93\u2013107","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"890_CR44","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2024.102347","volume":"122","author":"C Corea","year":"2024","unstructured":"Corea C, Kuhlmann I, Thimm M, Grant J (2024) Paraconsistent reasoning for inconsistency measurement in declarative process specifications. Inf Syst 122:102347","journal-title":"Inf Syst"},{"issue":"3","key":"890_CR45","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2338626.2338628","volume":"37","author":"E Damaggio","year":"2012","unstructured":"Damaggio E, Deutsch A, Vianu V (2012) Artifact systems with data dependencies and arithmetic. ACM Trans Database Syst 37(3):1\u201336","journal-title":"ACM Trans Database Syst"},{"issue":"4","key":"890_CR46","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3506799","volume":"31","author":"G De Giacomo","year":"2022","unstructured":"De Giacomo G, De Masellis R, Maggi FM, Montali M (2022) Monitoring constraints and metaconstraints with temporal logics on finite traces. ACM Trans Softw Eng Methodol 31(4):1\u201344","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"890_CR47","doi-asserted-by":"crossref","unstructured":"De\u00a0Giacomo G, Maggi FM, Marrella A, Patrizi F (2017) On the disruptive effectiveness of automated planning for ltlf-based trace alignment. In: Singh S, Markovitch S (eds) Proceedings of the Thirty-First AAAI conference on artificial intelligence (AAAI 2017). AAAI Press, pp. 3555\u20133561","DOI":"10.1609\/aaai.v31i1.11020"},{"key":"890_CR48","unstructured":"de Giacomo G, Vardi MY (2013) Linear temporal logic and linear dynamic logic on finite traces. In: Proc. 23rd IJCAI, pp. 854\u2013860"},{"key":"890_CR49","doi-asserted-by":"crossref","unstructured":"de Leoni M, Felli P, Montali M (2018) A holistic approach for soundness verification of decision-aware process models. In: Proceedings of ER 2018. LNCS, vol. 11157. Springer, pp. 219\u2013235","DOI":"10.1007\/978-3-030-00847-5_17"},{"key":"890_CR50","doi-asserted-by":"crossref","unstructured":"de Moura L, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Proc. 14th TACAS. LNCS, vol. 4963, pp. 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"890_CR51","doi-asserted-by":"crossref","unstructured":"de Moura L, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Proceedings of TACAS 2008. LNCS, vol. 4963. Springer, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"issue":"3","key":"890_CR52","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1507244.1507246","volume":"10","author":"S Demri","year":"2009","unstructured":"Demri S, Lazic R (2009) LTL with the freeze quantifier and register automata. ACM Trans Comput Log 10(3):1\u201330","journal-title":"ACM Trans Comput Log"},{"issue":"2","key":"890_CR53","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1145\/3212019.3212025","volume":"5","author":"A Deutsch","year":"2018","unstructured":"Deutsch A, Hull R, Li Y, Vianu V (2018) Automatic verification of database-centric systems. ACM SIGLOG News 5(2):37\u201356","journal-title":"ACM SIGLOG News"},{"issue":"3","key":"890_CR54","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3321487","volume":"44","author":"A Deutsch","year":"2019","unstructured":"Deutsch A, Li Y, Vianu V (2019) Verification of hierarchical artifact systems. ACM Trans Database Syst 44(3):1\u201368","journal-title":"ACM Trans Database Syst"},{"key":"890_CR55","doi-asserted-by":"crossref","unstructured":"Di\u00a0Francescomarino C, Ghidini C (2022) Predictive process monitoring. In: van\u00a0der Aalst WMP, Carmona J (eds) Process Mining Handbook. Lecture notes in business information processing, vol 448. Springer, pp 320\u2013346","DOI":"10.1007\/978-3-031-08848-3_10"},{"key":"890_CR56","doi-asserted-by":"crossref","unstructured":"Donadello I, Felli P, Innes C, Maggi FM, Montali M (2024) Conformance checking of fuzzy logs against declarative temporal specifications. In: Marrella A, Resinas M, Jans M, Rosemann M (eds) Proceedings of the 22nd international conference on business process management (BPM 2024). Lecture notes in computer science. vol 14940. Springer, pp 39\u201356","DOI":"10.1007\/978-3-031-70396-6_3"},{"key":"890_CR57","doi-asserted-by":"publisher","unstructured":"Dutertre B (2014) Yices 2.2. In: Biere A, Bloem R (eds) Proceedings of 26th CAV. Lecture notes in computer science, vol 8559. Springer, pp 737\u2013744. https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"890_CR58","doi-asserted-by":"crossref","unstructured":"Felli P, Gianola A, Montali M, Rivkin A, Winkler S (2021) CoCoMoT: conformance checking of multi-perspective processes via SMT. In: Proceedings of BPM 2021. LNCS, vol 12875. Springer, pp 217\u2013234","DOI":"10.1007\/978-3-030-85469-0_15"},{"key":"890_CR59","doi-asserted-by":"crossref","unstructured":"Felli P, Gianola A, Montali M, Rivkin A, Winkler S (2022) Conformance checking with uncertainty via SMT. In: Ciccio CD, Dijkman RM, del-Rio-Ortega A, Rinderle-Ma S (eds) Proceedings of 20th international conference on business process management (BPM 2022). Lecture notes in computer science, vol 13420. Springer, pp 199\u2013216","DOI":"10.1007\/978-3-031-16103-2_15"},{"key":"890_CR60","doi-asserted-by":"publisher","DOI":"10.1016\/J.IS.2023.102230","author":"P Felli","year":"2023","unstructured":"Felli P, Gianola A, Montali M, Rivkin A (2023) Winkler S Data-aware conformance checking with SMT. Inf Syst. https:\/\/doi.org\/10.1016\/J.IS.2023.102230","journal-title":"Inf Syst"},{"key":"890_CR61","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENGAPPAI.2023.106895","volume":"126","author":"P Felli","year":"2023","unstructured":"Felli P, Gianola A, Montali M, Rivkin A, Winkler S (2023) Multi-perspective conformance checking of uncertain process traces: an SMT-based approach. Eng Appl Artif Intell 126:106895. https:\/\/doi.org\/10.1016\/J.ENGAPPAI.2023.106895","journal-title":"Eng Appl Artif Intell"},{"key":"890_CR62","doi-asserted-by":"crossref","unstructured":"Felli P, de\u00a0Leoni M, Montali M (2019) Soundness verification of decision-aware process models with variable-to-variable conditions. In: Proceedings of ACSD 2019. IEEE, pp 82\u201391","DOI":"10.1109\/ACSD.2019.00013"},{"key":"890_CR63","doi-asserted-by":"crossref","unstructured":"Felli P, de\u00a0Leoni M, Montali M (2019) Soundness verification of decision-aware process models with variable-to-variable conditions. In: Proc. 19th ACSD. IEEE, pp 82\u201391","DOI":"10.1109\/ACSD.2019.00013"},{"key":"890_CR64","doi-asserted-by":"publisher","unstructured":"Felli P, Montali M, Patrizi F, Winkler S (2023) Monitoring arithmetic temporal properties on finite traces. In: Williams B, Chen Y, Neville J (eds) Proceedings of the 37th AAAI conference on artificial intelligence (AAAI 2023). AAAI Press, pp 6346\u20136354. https:\/\/doi.org\/10.1609\/AAAI.V37I5.25781","DOI":"10.1609\/AAAI.V37I5.25781"},{"key":"890_CR65","doi-asserted-by":"crossref","unstructured":"Felli P, Montali M, Winkler S (2022) CTL$$^{\\text{*}}$$ model checking for data-aware dynamic systems with arithmetic. In: Blanchette J, Kov\u00e1cs L, Pattinson D (eds) Proceedings of the 11th international joint conference on automated reasoning (IJCAR 2022). Lecture notes in computer science, vol 13385. Springer, pp 36\u201356","DOI":"10.1007\/978-3-031-10769-6_4"},{"key":"890_CR66","doi-asserted-by":"crossref","unstructured":"Felli P, Montali M, Winkler S (2022) Linear-time verification of data-aware dynamic systems with arithmetic. In: Proceedings of the 36th AAAI conference on artificial intelligence (AAAI 2022). AAAI Press, pp 5642\u20135650","DOI":"10.1609\/aaai.v36i5.20505"},{"key":"890_CR67","doi-asserted-by":"crossref","unstructured":"Felli P, Montali M, Winkler S (2022) Soundness of data-aware processes with arithmetic conditions. In: Franch X, Poels G, Gailly F, Snoeck M (eds) Proceedings of the 34th international conference on advanced information systems engineering (CAiSE 2022). Lecture notes in computer science, vol 13295. Springer, pp 389\u2013406","DOI":"10.1007\/978-3-031-07472-1_23"},{"key":"890_CR68","doi-asserted-by":"publisher","unstructured":"Felli P, Montali M, Winkler S (2023) Repairing soundness properties in data-aware processes. In: Proceedings of the 5th international conference on process mining (ICPM 2023). IEEE, pp 41\u201348. https:\/\/doi.org\/10.1109\/ICPM60904.2023.10271969","DOI":"10.1109\/ICPM60904.2023.10271969"},{"key":"890_CR69","doi-asserted-by":"crossref","unstructured":"Gal A (2023) Everything there is to know about stochastically known logs. In: Proceedings of the 5th international conference on process mining (ICPM 2023). IEEE, pp. xvii\u2013xxiii","DOI":"10.1109\/ICPM60904.2023.10271980"},{"key":"#cr-split#-890_CR70.1","doi-asserted-by":"crossref","unstructured":"Geatti L, Gianola A, Gigante N (2022) Linear temporal logic modulo theories over finite traces. In: L.D. Raedt","DOI":"10.24963\/ijcai.2022\/366"},{"key":"#cr-split#-890_CR70.2","unstructured":"(ed) Proceedings of the 31st international joint conference on artificial intelligence (IJCAI 2022). ijcai.org, pp 2641-2647"},{"key":"890_CR71","doi-asserted-by":"publisher","unstructured":"Geatti L, Gianola A, Gigante N, Winkler S (2023) Decidable fragments of LTL$$_{\\text{f }}$$ modulo theories. In: Gal K, Now\u00e9 A, Nalepa GJ, Fairstein R, Radulescu R (eds) Proceedings of ECAI 2023 - 26th European conference on artificial intelligence, Frontiers in Artificial Intelligence and Applications, vol 372. IOS Press, pp. 811\u2013818. https:\/\/doi.org\/10.3233\/FAIA230348","DOI":"10.3233\/FAIA230348"},{"key":"890_CR72","doi-asserted-by":"crossref","unstructured":"Ghilardi S, Gianola A, Montali M, Rivkin A (2021) Delta-BPMN: a concrete language and verifier for data-aware BPMN. In: Proceedings of BPM 2021. LNCS, vol 12875. Springer, pp 179\u2013196","DOI":"10.1007\/978-3-030-85469-0_13"},{"key":"890_CR73","doi-asserted-by":"publisher","DOI":"10.1016\/J.IS.2022.102011","author":"S Ghilardi","year":"2022","unstructured":"Ghilardi S, Gianola A, Montali M, Rivkin A (2022) Petri net-based object-centric processes with read-only data. Inf Syst. https:\/\/doi.org\/10.1016\/J.IS.2022.102011","journal-title":"Inf Syst"},{"key":"890_CR74","doi-asserted-by":"crossref","unstructured":"Ghilardi S, Gianola A, Montali M, Rivkin A (2023) Safety verification and universal invariants for relational action bases. In: Proceedings of the 32nd international joint conference on artificial intelligence (IJCAI 2023). ijcai.org, pp. 3248\u20133257","DOI":"10.24963\/ijcai.2023\/362"},{"key":"890_CR75","doi-asserted-by":"publisher","unstructured":"Gianola A (2023) Verification of data-aware processes via satisfiability modulo theories. LNBIP Springer. https:\/\/doi.org\/10.1007\/978-3-031-42746-6","DOI":"10.1007\/978-3-031-42746-6"},{"key":"890_CR76","doi-asserted-by":"publisher","unstructured":"Gianola A, Montali M, Winkler S (2023) Linear-time verification of data-aware processes modulo theories via covers and automata (extended version). CoRR abs\/2310.12180 https:\/\/doi.org\/10.48550\/ARXIV.2310.12180","DOI":"10.48550\/ARXIV.2310.12180"},{"key":"890_CR77","doi-asserted-by":"crossref","unstructured":"Gianola A, Montali M, Winkler S (2024) Linear-time verification of data-aware processes modulo theories via covers and automata. In: Wooldridge MJ, Dy JG, Natarajan S (eds) Proceedings of the 38th AAAI conference on artificial intelligence (AAAI 2024). AAAI Press, pp. 10525\u201310534","DOI":"10.1609\/aaai.v38i9.28922"},{"key":"890_CR78","doi-asserted-by":"crossref","unstructured":"Gianola A, Montali M, Winkler S (2024) Object-centric conformance alignments with synchronization. In: Guizzardi G, Santoro FM, Mouratidis H, Soffer P (eds) Proceedings of the 36th international conference on advanced information systems engineering (CAiSE 2024). Lecture notes in computer science, vol 14663. Springer, pp 3\u201319","DOI":"10.1007\/978-3-031-61057-8_1"},{"key":"890_CR79","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2019.101482","volume":"89","author":"V Leno","year":"2020","unstructured":"Leno V, Dumas M, Maggi FM, La Rosa M, Polyvyanyy A (2020) Automated discovery of declarative process models with correlated data conditions. Inf Syst 89:101482","journal-title":"Inf Syst"},{"key":"890_CR80","doi-asserted-by":"crossref","unstructured":"de\u00a0Leoni M, Felli P, Montali M (2018) A holistic approach for soundness verification of decision-aware process models. In: 37th ER. LNCS, vol 11157, pp 219\u2013235","DOI":"10.1007\/978-3-030-00847-5_17"},{"key":"890_CR81","doi-asserted-by":"crossref","unstructured":"de\u00a0Leoni M, Felli P, Montali M (2020) Strategy synthesis for data-aware dynamic systems with multiple actors. In: Proc. 17th KR, pp. 315\u2013325","DOI":"10.24963\/kr.2020\/32"},{"issue":"5","key":"890_CR82","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/j.jlap.2008.08.004","volume":"78","author":"M Leucker","year":"2009","unstructured":"Leucker M, Schallhart C (2009) A brief account of runtime verification. J Log Algebr Methods Program 78(5):293\u2013303. https:\/\/doi.org\/10.1016\/j.jlap.2008.08.004","journal-title":"J Log Algebr Methods Program"},{"key":"890_CR83","doi-asserted-by":"crossref","unstructured":"Li Y, Deutsch A, Vianu V (2017) VERIFAS: a practical verifier for artifact systems. PVLDB 11(3)","DOI":"10.14778\/3157794.3157798"},{"key":"890_CR84","doi-asserted-by":"crossref","unstructured":"Liss L, Adams JN, van\u00a0der Aalst WMP (2023) Object-centric alignments. In: Almeida JPA, Borbinha J, Guizzardi G, Link S, Zdravkovic J (eds) Proceedings of the 42nd international conference on conceptual modeling (ER 2023). Lecture notes in computer science, vol 14320. Springer, pp 201\u2013219","DOI":"10.1007\/978-3-031-47262-6_11"},{"key":"890_CR85","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/j.is.2015.02.007","volume":"54","author":"LT Ly","year":"2015","unstructured":"Ly LT, Maggi FM, Montali M, Rinderle-Ma S, van der Aalst WMP (2015) Compliance monitoring in business processes: functionalities, application, and tool-support. Inf Syst 54:209\u2013234","journal-title":"Inf Syst"},{"key":"890_CR86","doi-asserted-by":"crossref","unstructured":"Maggi FM, Dumas M, Garc\u00eda-Ba\u00f1uelos L, Montali M (2013) Discovering data-aware declarative process models from event logs. In: Daniel F, Wang J, Weber B (eds) Proceedings of the 11th international conference on business process management (BPM 2013). Lecture notes in computer science, vol 8094. Springer, pp 81\u201396","DOI":"10.1007\/978-3-642-40176-3_8"},{"key":"890_CR87","doi-asserted-by":"crossref","unstructured":"Maggi FM, Westergaard M, Montali M. van\u00a0der Aalst WMP (2011) Runtime verification of ltl-based declarative process models. In: Khurshid S, Sen K (eds) Proceedings of the 2nd international conference on runtime verification (RV 2011). Lecture notes in computer science, vol 7186. Springer, pp 131\u2013146","DOI":"10.1007\/978-3-642-29860-8_11"},{"key":"890_CR88","unstructured":"Mannhardt F (2018) Multi-perspective process mining. Ph.D. thesis, Technical University of Eindhoven"},{"key":"890_CR89","doi-asserted-by":"crossref","unstructured":"Mannhardt F, de Leoni M, Reijers HA, van der Aalst W (2016) Decision mining revisited: discovering overlapping rules. In: 28th CAiSE. LNCS, vol 9694, pp 377\u2013392","DOI":"10.1007\/978-3-319-39696-5_23"},{"issue":"4","key":"890_CR90","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/s00607-015-0441-1","volume":"98","author":"F Mannhardt","year":"2016","unstructured":"Mannhardt F, de Leoni M, Reijers H, van der Aalst W (2016) Balanced multi-perspective checking of process conformance. Computing 98(4):407\u2013437","journal-title":"Computing"},{"issue":"4","key":"890_CR91","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/s00607-015-0441-1","volume":"98","author":"F Mannhardt","year":"2016","unstructured":"Mannhardt F, de Leoni M, Reijers HA, van der Aalst WMP (2016) Balanced multi-perspective checking of process conformance. Computing 98(4):407\u2013437","journal-title":"Computing"},{"key":"890_CR92","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2023.104062","volume":"328","author":"G Marra","year":"2024","unstructured":"Marra G, Dumancic S, Manhaeve R, De Raedt L (2024) From statistical relational to neurosymbolic artificial intelligence: a survey. Artif Intell 328:104062","journal-title":"Artif Intell"},{"key":"890_CR93","unstructured":"Microsoft Research: The Z3 Prover. https:\/\/github.com\/Z3Prover\/z3"},{"key":"890_CR94","doi-asserted-by":"crossref","unstructured":"Montali M (2024) AI for declarative processes: representation, mining, synthesis. In: Endriss U, Melo FS, Bach K, Bugar\u00edn\u00a0Diz AJ, Alonso-Moral JM, Barro S, Heintz F (eds) Proceedings of the 27th European conference on artificial intelligence (ECAI 2024). Frontiers in artificial intelligence and applications, vol 392. IOS Press, pp 17\u201324","DOI":"10.3233\/FAIA240461"},{"key":"890_CR95","doi-asserted-by":"crossref","unstructured":"Montali M, Chesani F, Mello P, Maggi FM (2013) Towards data-aware constraints in declare. In: Shin SY, Maldonado JC (eds) Proceedings of the 28th annual ACM symposium on applied computing (SAC \u201913). ACM, pp 1391\u20131396","DOI":"10.1145\/2480362.2480624"},{"key":"890_CR96","doi-asserted-by":"crossref","unstructured":"Montali M, Winkler S (2024) Relating behaviour of data-aware process models. p. 102363","DOI":"10.1016\/j.datak.2024.102363"},{"key":"890_CR97","doi-asserted-by":"publisher","DOI":"10.1016\/J.IS.2021.101810","volume":"102","author":"M Pegoraro","year":"2021","unstructured":"Pegoraro M, Uysal MS, van der Aalst WMP (2021) Conformance checking over uncertain event data. Inf Syst 102:101810. https:\/\/doi.org\/10.1016\/J.IS.2021.101810","journal-title":"Inf Syst"},{"key":"890_CR98","doi-asserted-by":"publisher","unstructured":"Polyvyanyy A, van\u00a0der Werf JMEM, Overbeek S, Brouwers R (2019) Information systems modeling: language, verification, and tool support. In: Giorgini P, Weber B (eds) Advanced information systems engineering - 31st international conference, CAiSE 2019, Rome, Italy, June 3-7, 2019, Proceedings. Lecture notes in computer science, vol 11483. Springer, pp 194\u2013212https:\/\/doi.org\/10.1007\/978-3-030-21290-2_13","DOI":"10.1007\/978-3-030-21290-2_13"},{"key":"890_CR99","doi-asserted-by":"crossref","unstructured":"Reichert M (2012) Process and data: two sides of the same coin? In: OTM 2012. LNCS, vol 7565, pp 2\u201319","DOI":"10.1007\/978-3-642-33606-5_2"},{"key":"890_CR100","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1613\/jair.1.15313","volume":"80","author":"M Roveri","year":"2024","unstructured":"Roveri M, Ciccio CD, Di Francescomarino C, Ghidini C (2024) Computing unsatisfiable cores for ltlf specifications. J Artif Intell Res 80:517\u2013558","journal-title":"J Artif Intell Res"},{"issue":"2","key":"890_CR101","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2699915","volume":"16","author":"R Sebastiani","year":"2015","unstructured":"Sebastiani R, Tomasi S (2015) Optimization modulo theories with linear rational costs. ACM Trans Comput Log 16(2):1\u201343. https:\/\/doi.org\/10.1145\/2699915","journal-title":"ACM Trans Comput Log"},{"issue":"3","key":"890_CR102","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/S10817-018-09508-6","volume":"64","author":"R Sebastiani","year":"2020","unstructured":"Sebastiani R, Trentin P (2020) Optimathsat: a tool for optimization modulo theories. J Autom Reason 64(3):423\u2013460. https:\/\/doi.org\/10.1007\/S10817-018-09508-6","journal-title":"J Autom Reason"},{"issue":"4","key":"890_CR103","doi-asserted-by":"publisher","first-page":"2679","DOI":"10.1007\/s10270-018-0695-0","volume":"18","author":"S Steinau","year":"2019","unstructured":"Steinau S, Marrella A, Andrews K, Leotta F, Mecella M, Reichert M (2019) DALEC: a framework for the systematic evaluation of data-centric approaches to process management software. Softw Syst Model 18(4):2679\u20132716","journal-title":"Softw Syst Model"},{"key":"890_CR104","unstructured":"Sturm C, Sch\u00f6nig S, Ciccio CD (2017) Distributed multi-perspective declare discovery. In: Claris\u00f3 R, Leopold H, Mendling J, van\u00a0der Aalst WMP, Kumar A, Pentland BT, Weske M (eds) Proceedings of the BPM demo track and BPM dissertation award. CEUR workshop proceedings, vol 1920. CEUR-WS.org"},{"key":"890_CR105","doi-asserted-by":"crossref","unstructured":"Umili E, Argenziano F, Capobianco R (2024) Neural reward machines. In: Endriss U, Melo FS, Bach K, Bugar\u00edn\u00a0Diz AJ, Alonso-Moral JM, Barro S, Heintz F (eds) Proceedings of the 27th European conference on artificial intelligence (ECAI 2024). Frontiers in artificial intelligence and applications, vol 392. IOS Press, pp 3055\u20133062","DOI":"10.3233\/FAIA240847"},{"key":"890_CR106","doi-asserted-by":"crossref","unstructured":"Umili E, Capobianco R, De\u00a0Giacomo G (2023) Grounding ltlf specifications in image sequences. In: Marquis P, Son TC, Kern-Isberner G (eds) Proceedings of the 20th international conference on principles of knowledge representation and reasoning (KR 2023), pp 668\u2013678","DOI":"10.24963\/kr.2023\/65"},{"key":"890_CR107","unstructured":"Umili E, Licks GP, Patrizi F (2024) Enhancing deep sequence generation with logical temporal knowledge. In: Giacomo GD, Fionda V, Fournier F, Ielo A, Limonad L, Montali M (eds) Proceedings of the 3rd international workshop on process management in the AI Era (PMAI 2024). CEUR workshop proceedings, vol 3779. CEUR-WS.org, pp 23\u201334"},{"key":"890_CR108","doi-asserted-by":"crossref","unstructured":"Zavatteri M, Bresolin D, de\u00a0Leoni M (2023) Repair of unsound data-aware process models. In: De\u00a0Weerdt J, Pufahl L (eds) Proceedings of the 2023 business process management workshops. Lecture notes in business information processing, vol 492. Springer, pp 383\u2013395","DOI":"10.1007\/978-3-031-50974-2_29"}],"container-title":["KI - K\u00fcnstliche Intelligenz"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s13218-025-00890-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s13218-025-00890-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s13218-025-00890-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,20]],"date-time":"2025-10-20T19:02:17Z","timestamp":1760986937000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s13218-025-00890-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,29]]},"references-count":109,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["890"],"URL":"https:\/\/doi.org\/10.1007\/s13218-025-00890-z","relation":{},"ISSN":["0933-1875","1610-1987"],"issn-type":[{"value":"0933-1875","type":"print"},{"value":"1610-1987","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,29]]},"assertion":[{"value":"9 December 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 March 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 April 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}