{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T21:16:54Z","timestamp":1780607814377,"version":"3.54.1"},"publisher-location":"Cham","reference-count":99,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031088476","type":"print"},{"value":"9783031088483","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,6,27]],"date-time":"2022-06-27T00:00:00Z","timestamp":1656288000000},"content-version":"vor","delay-in-days":177,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The declarative specification of business processes is based upon the elicitation of behavioural rules that constrain the legal executions of the process. The carry-out of the process is up to the actors, who can vary the execution dynamics as long as they do not violate the constraints imposed by the declarative model. The constraints specify the conditions that require, permit or forbid the execution of activities, possibly depending on the occurrence (or absence) of other ones. In this chapter, we review the main techniques for process mining using declarative process specifications, which we call <jats:italic>declarative process mining<\/jats:italic>. In particular, we focus on three fundamental tasks of (1) reasoning on declarative process specifications, which is in turn instrumental to their (2) discovery from event logs and their (3) monitoring against running process executions to promptly detect violations. We ground our review on Declare, one of the most widely studied declarative process specification languages. Thanks to the fact that Declare can be formalized using temporal logics over finite traces, we exploit the automata-theoretic characterization of such logics as the core, unified algorithmic basis to tackle reasoning, discovery, and monitoring. We conclude the chapter with a discussion on recent advancements in declarative process mining, considering in particular multi-perspective extensions of the original approach.<\/jats:p>","DOI":"10.1007\/978-3-031-08848-3_4","type":"book-chapter","created":{"date-parts":[[2022,6,26]],"date-time":"2022-06-26T23:02:48Z","timestamp":1656284568000},"page":"108-152","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":46,"title":["Declarative Process Specifications: Reasoning, Discovery, Monitoring"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0955-6940","authenticated-orcid":false,"given":"Claudio","family":"Di Ciccio","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8021-3430","authenticated-orcid":false,"given":"Marco","family":"Montali","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,6,27]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"van der Aalst, W.M.P.: Process mining: a 360 degrees overview. In: van der Aalst, W.M.P., Carmona, J. (eds.) Process Mining Handbook. LNBIP, vol. 448, pp. xx\u2013yy. Springer, Cham (2022)","DOI":"10.1007\/978-3-031-08848-3"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"van der Aalst, W.M.P.: Foundations of process discovery. In: van der Aalst, W.M.P., Carmona, J. (eds.) Process Mining Handbook. LNBIP, vol. 448, pp. xx\u2013yy. Springer, Cham (2022)","DOI":"10.1007\/978-3-031-08848-3"},{"key":"4_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0085-4","volume-title":"Data Mining for Association Rules and Sequential Patterns - Sequential and Parallel Algorithms","author":"J-M Adamo","year":"2001","unstructured":"Adamo, J.-M.: Data Mining for Association Rules and Sequential Patterns - Sequential and Parallel Algorithms. Springer, New York (2001). https:\/\/doi.org\/10.1007\/978-1-4613-0085-4"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-030-85469-0_3","volume-title":"Business Process Management","author":"A Alman","year":"2021","unstructured":"Alman, A., Di Ciccio, C., Maggi, F.M., Montali, M., van der Aa, H.: RuM: declarative process mining, distilled. In: Polyvyanyy, A., Wynn, M.T., Van Looy, A., Reichert, M. (eds.) BPM 2021. LNCS, vol. 12875, pp. 23\u201329. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85469-0_3"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Alman, A., Maggi, F.M., Montali, M., Patrizi, F., Rivkin, A.: Multi-model monitoring framework for hybrid process specifications. In: Franch, X., Poels, G. (eds.) Proceedings of the 34th International Conference on Advanced Information Systems Engineering (CAiSE 2022). Lecture Notes in Computer Science (2022, to appear)","DOI":"10.1007\/978-3-031-07472-1_19"},{"key":"4_CR6","unstructured":"Alman, A., Maggi, F.M., Montali, M., Pe\u00f1aloza, R.: Probabilistic declarative process mining. Inf. Syst. (2012, to appear)"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-030-26619-6_11","volume-title":"Business Process Management","author":"A Artale","year":"2019","unstructured":"Artale, A., Kovtunova, A., Montali, M., van\u00a0der Aalst, W.M.P.: Modeling and reasoning over declarative data-aware processes with object-centric behavioral constraints. In: Hildebrandt, T., van Dongen, B.F., R\u00f6glinger, M., Mendling, J. (eds.) BPM 2019. LNCS, vol. 11675, pp. 139\u2013156. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-26619-6_11"},{"key":"4_CR8","unstructured":"Back, C.O., Slaats, T., Hildebrandt, T.T., Marquard, M.: Discover: Accurate & efficient discovery of declarative process models. CoRR, abs\/2005.10085 (2020)"},{"issue":"2","key":"4_CR9","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s10270-017-0603-z","volume":"17","author":"T Baier","year":"2018","unstructured":"Baier, T., Di Ciccio, C., Mendling, J., Weske, M.: Matching events and activities by integrating behavioral aspects and label analysis. Softw. Syst. Model. 17(2), 573\u2013598 (2018)","journal-title":"Softw. Syst. Model."},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Basin, D.A., Klaedtke, F., M\u00fcller, S., Zalinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 15:1\u201315:45 (2015)","DOI":"10.1145\/2699444"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1\u201314:64 (2011)","DOI":"10.1145\/2000799.2000800"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-030-85469-0_16","volume-title":"Business Process Management","author":"G Bergami","year":"2021","unstructured":"Bergami, G., Maggi, F.M., Marrella, A., Montali, M.: Aligning data-aware declarative process models and event logs. In: Polyvyanyy, A., Wynn, M.T., Van Looy, A., Reichert, M. (eds.) BPM 2021. LNCS, vol. 12875, pp. 235\u2013251. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85469-0_16"},{"key":"4_CR13","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, F.M., Sperduti, A.: Conformance checking based on multi-perspective declarative process models. Expert Syst. Appl. 65, 194\u2013211 (2016)","journal-title":"Expert Syst. Appl."},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Calvanese, D., De Giacomo, G., Montali, M., Patrizi, F.: Verification and monitoring for first-order LTL with persistence-preserving quantification over finite and infinite traces. In: De Raedt, L. (ed.) Proceedings of the 31st International Joint Conference on Artificial Intelligence (IJCAI 2022). ijcai.org (2022, to appear)","DOI":"10.24963\/ijcai.2022\/354"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Camacho, A., McIlraith, S.A.: Learning interpretable models expressed in linear temporal logic. In: Benton, J., Lipovetzky, N., Onaindia, E., Smith, D.E., Srivastava, S. (eds.) Proceedings of the Twenty-Ninth International Conference on Automated Planning and Scheduling (ICAPS 2018), pp. 621\u2013630. AAAI Press (2019)","DOI":"10.1609\/icaps.v29i1.3529"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Carmona, J., van Dongen, B., Weidlich, M.: Conformance checking: foundations, milestones and challenges. In: van der Aalst, W.M.P., Carmona, J. (eds.) Process Mining Handbook. LNBIP, vol. 448, pp. xx\u2013yy. Springer, Cham (2022)","DOI":"10.1007\/978-3-031-08848-3_5"},{"key":"4_CR17","unstructured":"Cecconi, A., De Giacomo, G., Di Ciccio, C., Mendling, J.: A temporal logic-based measurement framework for process mining. In: van Dongen et al. [92]"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-319-98648-7_8","volume-title":"Business Process Management","author":"A Cecconi","year":"2018","unstructured":"Cecconi, A., Di Ciccio, C., De Giacomo, G., Mendling, J.: Interestingness of traces in declarative process mining: the janus LTLp$$_f$$ approach. In: Weske, M., Montali, M., Weber, I., vom Brocke, J. (eds.) BPM 2018. LNCS, vol. 11080, pp. 121\u2013138. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-98648-7_8"},{"key":"4_CR19","unstructured":"Chesani, F., et al.: Process discovery on deviant traces and other stranger things. CoRR, abs\/2109.14883 (2021)"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-00899-3_16","volume-title":"Transactions on Petri Nets and Other Models of Concurrency II","author":"F Chesani","year":"2009","unstructured":"Chesani, F., Lamma, E., Mello, P., Montali, M., Riguzzi, F., Storari, S.: Exploiting inductive logic programming techniques for declarative process mining. In: Jensen, K., van der Aalst, W.M.P. (eds.) Transactions on Petri Nets and Other Models of Concurrency II. LNCS, vol. 5460, pp. 278\u2013295. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00899-3_16"},{"key":"4_CR21","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-00899-3_16","volume":"2","author":"F Chesani","year":"2009","unstructured":"Chesani, F., Lamma, E., Mello, P., Montali, M., Riguzzi, F., Storari, S.: Exploiting inductive logic programming techniques for declarative process mining. Trans. Petri Nets Other Model. Concurr. 2, 278\u2013295 (2009)","journal-title":"Trans. Petri Nets Other Model. Concurr."},{"issue":"2","key":"4_CR22","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/S0019-9958(58)90082-2","volume":"1","author":"N Chomsky","year":"1958","unstructured":"Chomsky, N., Miller, G.A.: Finite state languages. Inf. Control 1(2), 91\u2013112 (1958)","journal-title":"Inf. Control"},{"key":"4_CR23","unstructured":"Corea, C., Deisen, M., Delfmann, P.: Resolving inconsistencies in declarative process models based on culpability measurement. In: Ludwig, T., Pipek, V. (eds.) WI, pp. 139\u2013153. University of Siegen, Germany\/AISeL (2019)"},{"key":"4_CR24","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-030-26643-1_2","volume-title":"Business Process Management Forum","author":"C Corea","year":"2019","unstructured":"Corea, C., Delfmann, P.: Quasi-inconsistency in declarative process models. In: Hildebrandt, T., van Dongen, B.F., R\u00f6glinger, M., Mendling, J. (eds.) BPM 2019. LNBIP, vol. 360, pp. 20\u201335. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-26643-1_2"},{"key":"4_CR25","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-85440-9_1","volume-title":"Business Process Management Forum","author":"C Corea","year":"2021","unstructured":"Corea, C., Nagel, S., Mendling, J., Delfmann, P.: Interactive and minimal repair of declarative process models. In: Polyvyanyy, A., Wynn, M.T., Van Looy, A., Reichert, M. (eds.) BPM 2021. LNBIP, vol. 427, pp. 3\u201319. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85440-9_1"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Davulcu, H., Kifer, M., Ramakrishnan, C.R., Ramakrishnan, I.V.: Logic based modeling and analysis of workflows. In: PODS, pp. 25\u201333. ACM (1998)","DOI":"10.1145\/275487.275491"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-10172-9_1","volume-title":"Business Process Management","author":"G De Giacomo","year":"2014","unstructured":"De Giacomo, G., De Masellis, R., Grasso, M., Maggi, F.M., Montali, M.: Monitoring business metaconstraints based on LTL and LDL for finite traces. In: Sadiq, S., Soffer, P., V\u00f6lzer, H. (eds.) BPM 2014. LNCS, vol. 8659, pp. 1\u201317. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10172-9_1"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"De Giacomo, G., De Masellis, R., Maggi, F.M., Montali, M.: Monitoring constraints and metaconstraints with temporal logics on finite traces. ACM Trans. Softw. Eng. Methodol. (2022, to appear)","DOI":"10.1145\/3506799"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"De Giacomo, G., De Masellis, R., Montali, M.: Reasoning on LTL on finite traces: insensitivity to infiniteness. In: Brodley, C.E., Stone, P. (eds.) AAAI, pp. 1027\u20131033. AAAI Press (2014)","DOI":"10.1609\/aaai.v28i1.8872"},{"key":"4_CR30","unstructured":"De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Rossi, F. (ed.) IJCAI, pp. 854\u2013860. IJCAI\/AAAI (2013)"},{"key":"4_CR31","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1016\/j.is.2013.12.005","volume":"47","author":"M De Leoni","year":"2015","unstructured":"De Leoni, M., Maggi, F.M., van der Aalst, W.M.: An alignment-based framework to check the conformance of declarative process models and to preprocess event-log data. Inf. Syst. 47, 258\u2013277 (2015)","journal-title":"Inf. Syst."},{"issue":"Part 1","key":"4_CR32","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1016\/j.is.2018.01.001","volume":"74","author":"J De Smedt","year":"2018","unstructured":"De Smedt, J., De Weerdt, J., Serral, E., Vanthienen, J.: Discovering hidden dependencies in constraint-based declarative process models for improving understandability. Inf. Syst. 74(Part 1), 40\u201352 (2018)","journal-title":"Inf. Syst."},{"issue":"1","key":"4_CR33","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/s12599-015-0416-y","volume":"58","author":"J De Smedt","year":"2016","unstructured":"De Smedt, J., De Weerdt, J., Vanthienen, J., Poels, G.: Mixed-paradigm process modeling with intertwined state spaces. Bus. Inf. Syst. Eng. 58(1), 19\u201329 (2016)","journal-title":"Bus. Inf. Syst. Eng."},{"key":"4_CR34","doi-asserted-by":"crossref","unstructured":"Demri, S., Lazic, R.: LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10(3), 16:1\u201316:30 (2009)","DOI":"10.1145\/1507244.1507246"},{"issue":"1","key":"4_CR35","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.ic.2006.08.003","volume":"205","author":"S Demri","year":"2007","unstructured":"Demri, S., Lazic, R., Nowak, D.: On the freeze quantifier in constraint LTL: decidability and complexity. Inf. Comput. 205(1), 2\u201324 (2007)","journal-title":"Inf. Comput."},{"key":"4_CR36","unstructured":"Di Ciccio, C.: On the mining of artful processes. Ph.D. thesis, SAPIENZA, University of Rome, October 2013"},{"key":"4_CR37","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-24626-0_2","volume-title":"Enterprise and Organizational Modeling and Simulation","author":"C Di Ciccio","year":"2015","unstructured":"Di Ciccio, C., Bernardi, M.L., Cimitile, M., Maggi, F.M.: Generating event logs through the simulation of declare models. In: Barjis, J., Pergl, R., Babkin, E. (eds.) EOMAS 2015. LNBIP, vol. 231, pp. 20\u201336. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24626-0_2"},{"key":"4_CR38","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1016\/j.is.2016.09.005","volume":"64","author":"C Di Ciccio","year":"2017","unstructured":"Di Ciccio, C., Maggi, F.M., Montali, M., Mendling, J.: Resolving inconsistencies and redundancies in declarative process models. Inf. Syst. 64, 425\u2013446 (2017)","journal-title":"Inf. Syst."},{"key":"4_CR39","doi-asserted-by":"crossref","unstructured":"Di Ciccio, C., Maggi, F.M., Montali, M., Mendling, J.: On the relevance of a business constraint to an event log. Inf. Syst. 78, 144\u2013161 (2018)","DOI":"10.1016\/j.is.2018.01.011"},{"key":"4_CR40","doi-asserted-by":"crossref","unstructured":"Di Ciccio, C., Mecella, M.: On the discovery of declarative control flows for artful processes. ACM Trans. Manag. Inf. Syst. 5(4), 24:1\u201324:37 (2015)","DOI":"10.1145\/2629447"},{"key":"4_CR41","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Boehm, B.W., Garlan, D., Kramer, J. (eds.) ICSE, pp. 411\u2013420. ACM (1999)","DOI":"10.1145\/302405.302672"},{"issue":"1","key":"4_CR42","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/s10270-014-0395-3","volume":"15","author":"A Elgammal","year":"2014","unstructured":"Elgammal, A., Turetken, O., van den Heuvel, W.-J., Papazoglou, M.: Formalizing and appling compliance patterns for business process compliance. Softw. Syst. Model. 15(1), 119\u2013146 (2014). https:\/\/doi.org\/10.1007\/s10270-014-0395-3","journal-title":"Softw. Syst. Model."},{"key":"4_CR43","doi-asserted-by":"crossref","unstructured":"Fahland, D.: Process mining over multiple behavioral dimensions with event knowledge graphs. In: van der Aalst, W.M.P., Carmona, J. (eds.) Process Mining Handbook. LNBIP, vol. 448, pp. xx\u2013yy. Springer, Cham (2022)","DOI":"10.1007\/978-3-031-08848-3_9"},{"key":"4_CR44","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1613\/jair.1.11256","volume":"63","author":"V Fionda","year":"2018","unstructured":"Fionda, V., Greco, V.: LTL on finite and process traces: complexity results and a practical reasoner. J. Artif. Intell. Res. 63, 557\u2013623 (2018)","journal-title":"J. Artif. Intell. Res."},{"issue":"5","key":"4_CR45","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1109\/TKDE.2019.2897309","volume":"32","author":"V Fionda","year":"2020","unstructured":"Fionda, V., Guzzo, A.: Control-flow modeling with declare: behavioral properties, computational complexity, and tools. IEEE Trans. Knowl. Data Eng. 32(5), 98\u2013911 (2020)","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"4_CR46","first-page":"1305","volume":"10","author":"S Goedertier","year":"2009","unstructured":"Goedertier, S., Martens, D., Vanthienen, J., Baesens, B.: Robust process discovery with artificial negative events. J. Mach. Learn. Res. 10, 1305\u20131340 (2009)","journal-title":"J. Mach. Learn. Res."},{"issue":"2","key":"4_CR47","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1006\/jvlc.1996.0009","volume":"7","author":"TRG Green","year":"1996","unstructured":"Green, T.R.G., Petre, M.: Usability analysis of visual programming environments: a \u2018cognitive dimensions\u2019 framework. Vis. Comp. and Lang. 7(2), 131\u201374 (1996)","journal-title":"Vis. Comp. and Lang."},{"issue":"2","key":"4_CR48","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/s10270-014-0435-z","volume":"15","author":"C Haisjackl","year":"2016","unstructured":"Haisjackl, C., et al.: Understanding declare models: strategies, pitfalls, empirical results. Softw. Syst. Model. 15(2), 325\u2013352 (2016)","journal-title":"Softw. Syst. Model."},{"key":"4_CR49","doi-asserted-by":"crossref","unstructured":"Hildebrandt, T.T., Mukkamala, R.R.: Declarative event-based workflow as distributed dynamic condition response graphs. In: PLACES. EPTCS, vol. 69, pp. 59\u201373 (2010)","DOI":"10.4204\/EPTCS.69.5"},{"key":"4_CR50","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"JE Hopcroft","year":"2006","unstructured":"Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation, 3rd edn. Addison-Wesley Longman Publishing Co. Inc., Boston (2006)","edition":"3"},{"issue":"2","key":"4_CR51","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O Kupferman","year":"2003","unstructured":"Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. Int. J. Softw. Tools Technol. Transfer 4(2), 224\u2013233 (2003)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"4_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-540-75183-0_25","volume-title":"Business Process Management","author":"E Lamma","year":"2007","unstructured":"Lamma, E., Mello, P., Montali, M., Riguzzi, F., Storari, S.: Inducing declarative logic-based models from labeled traces. In: Alonso, G., Dadam, P., Rosemann, M. (eds.) BPM 2007. LNCS, vol. 4714, pp. 344\u2013359. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75183-0_25"},{"key":"4_CR53","doi-asserted-by":"crossref","unstructured":"Lemieux, C., Park, D., Beschastnikh, I.: General LTL specification mining (T). In: Cohen, M.B., Grunske, L., Whalen, M. (eds.) 30th IEEE\/ACM International Conference on Automated Software Engineering, ASE 2015, Lincoln, NE, USA, 9\u201313 November 2015, pp. 81\u201392. IEEE Computer Society (2015)","DOI":"10.1109\/ASE.2015.71"},{"key":"4_CR54","doi-asserted-by":"publisher","DOI":"10.1016\/j.is.2019.101482","volume":"89","author":"V Leno","year":"2020","unstructured":"Leno, V., Dumas, M., Maggi, F.M., La Rosa, M., Polyvyanyy, A.: Automated discovery of declarative process models with correlated data conditions. Inf. Syst. 89, 101482 (2020)","journal-title":"Inf. Syst."},{"key":"4_CR55","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-319-59336-4_4","volume-title":"Business Information Systems","author":"G Li","year":"2017","unstructured":"Li, G., de Carvalho, R.M., van der Aalst, W.M.P.: Automatic discovery of object-centric behavioral constraint models. In: Abramowicz, W. (ed.) BIS 2017. LNBIP, vol. 288, pp. 43\u201358. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-59336-4_4"},{"key":"4_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/3-540-15648-8_16","volume-title":"Logics of Programs","author":"O Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol. 193, pp. 196\u2013218. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/3-540-15648-8_16"},{"key":"4_CR57","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/j.is.2015.02.007","volume":"54","author":"LT Ly","year":"2015","unstructured":"Ly, L.T., Maggi, F.M., Montali, M., Rinderle-Ma, S., van der Aalst, W.M.P.: Compliance monitoring in business processes: functionalities, application, and tool-support. Inf. Syst. 54, 209\u2013234 (2015)","journal-title":"Inf. Syst."},{"key":"4_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-642-31095-9_18","volume-title":"Advanced Information Systems Engineering","author":"FM Maggi","year":"2012","unstructured":"Maggi, F.M., Bose, R.P.J.C., van der Aalst, W.M.P.: Efficient discovery of understandable declarative process models from event logs. In: Ralyt\u00e9, J., Franch, X., Brinkkemper, S., Wrycza, S. (eds.) CAiSE 2012. LNCS, vol. 7328, pp. 270\u2013285. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31095-9_18"},{"key":"4_CR59","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1016\/j.is.2017.12.002","volume":"74","author":"FM Maggi","year":"2018","unstructured":"Maggi, F.M., Di Ciccio, C., Di Francescomarino, C., Kala, T.: Parallel algorithms for the automated discovery of declarative process models. Inf. Syst. 74, 136\u2013152 (2018)","journal-title":"Inf. Syst."},{"key":"4_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-642-40176-3_8","volume-title":"Business Process Management","author":"FM Maggi","year":"2013","unstructured":"Maggi, F.M., Dumas, M., Garc\u00eda-Ba\u00f1uelos, L., Montali, M.: Discovering data-aware declarative process models from event logs. In: Daniel, F., Wang, J., Weber, B. (eds.) BPM 2013. LNCS, vol. 8094, pp. 81\u201396. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40176-3_8"},{"key":"4_CR61","doi-asserted-by":"crossref","unstructured":"Maggi, F.M., Montali, M., Pe\u00f1aloza, R.: Temporal logics over finite traces with uncertainty. In: Proceedings of the 34 AAAI Conference on Artificial Intelligence (AAAI 2020), pp. 10218\u201310225. AAAI Press (2020)","DOI":"10.1609\/aaai.v34i06.6583"},{"key":"4_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-030-58666-9_3","volume-title":"Business Process Management","author":"FM Maggi","year":"2020","unstructured":"Maggi, F.M., Montali, M., Pe\u00f1aloza, R., Alman, A.: Extending temporal business constraints with uncertainty. In: Fahland, D., Ghidini, C., Becker, J., Dumas, M. (eds.) BPM 2020. LNCS, vol. 12168, pp. 35\u201354. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58666-9_3"},{"key":"4_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-28872-2_11","volume-title":"Fundamental Approaches to Software Engineering","author":"FM Maggi","year":"2012","unstructured":"Maggi, F.M., Montali, M., van der Aalst, W.M.P.: An operational decision support framework for monitoring business constraints. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 146\u2013162. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28872-2_11"},{"key":"4_CR64","doi-asserted-by":"crossref","unstructured":"Maggi, F.M., Montali, M., Westergaard, M., van der Aalst, W.M.P.: Monitoring business constraints with linear temporal logic: an approach based on colored automata. In: Rinderle-Ma et al. [81], pp. 132\u2013147","DOI":"10.1007\/978-3-642-23059-2_13"},{"key":"4_CR65","doi-asserted-by":"crossref","unstructured":"Maggi, F.M., Mooij, A.J., van der Aalst, W.M.P.: User-guided discovery of declarative process models. In: CIDM, pp. 192\u2013199. IEEE (2011)","DOI":"10.1109\/CIDM.2011.5949297"},{"key":"4_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-29860-8_11","volume-title":"Runtime Verification","author":"FM Maggi","year":"2012","unstructured":"Maggi, F.M., Westergaard, M., Montali, M., van der Aalst, W.M.P.: Runtime verification of LTL-based declarative process models. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 131\u2013146. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-29860-8_11"},{"key":"4_CR67","doi-asserted-by":"crossref","unstructured":"Montali, M.: Specification and verification of declarative open interaction models - a logic-based framework. Ph.D. thesis, University of Bologna, Italy (2009)","DOI":"10.1007\/978-3-642-14538-4"},{"key":"4_CR68","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14538-4","volume-title":"Specification and Verification of Declarative Open Interaction Models: a Logic-Based Approach","author":"M Montali","year":"2010","unstructured":"Montali, M.: Specification and Verification of Declarative Open Interaction Models: a Logic-Based Approach. Lecture Notes in Business Information Processing, vol. 56. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14538-4"},{"key":"4_CR69","doi-asserted-by":"crossref","unstructured":"Montali, M., Maggi, F.M., Chesani, F., Mello, P., van der Aalst, W.M.P.: Monitoring business constraints with the event calculus. ACM TIST 5(1), 17:1\u201317:30 (2013)","DOI":"10.1145\/2542182.2542199"},{"issue":"1","key":"4_CR70","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1658373.1658376","volume":"4","author":"M Montali","year":"2010","unstructured":"Montali, M., Pesic, M., van der Aalst, W.M.P., Chesani, F., Mello, P., Storari, S.: Declarative specification and verification of service choreographies. TWEB 4(1), 1\u201362 (2010)","journal-title":"TWEB"},{"key":"4_CR71","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-540-89982-2_39","volume-title":"Logic Programming","author":"M Montali","year":"2008","unstructured":"Montali, M., et al.: Verification from declarative specifications using logic programming. In: Garcia de la Banda, M., Pontelli, E. (eds.) ICLP 2008. LNCS, vol. 5366, pp. 440\u2013454. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-89982-2_39"},{"key":"4_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-540-78238-4_35","volume-title":"Business Process Management Workshops","author":"N Mulyar","year":"2008","unstructured":"Mulyar, N., Pesic, M., van der Aalst, W.M.P., Peleg, M.: Declarative and procedural approaches for modelling clinical guidelines: addressing flexibility issues. In: ter Hofstede, A., Benatallah, B., Paik, H.-Y. (eds.) BPM 2007. LNCS, vol. 4928, pp. 335\u2013346. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78238-4_35"},{"key":"4_CR73","doi-asserted-by":"publisher","DOI":"10.1016\/j.jbi.2022.103994","volume":"127","author":"J Munoz-Gama","year":"2022","unstructured":"Munoz-Gama, J., Martin, N., et al.: Process mining for healthcare: characteristics and challenges. J. Biomed. Inform. 127, 103994 (2022)","journal-title":"J. Biomed. Inform."},{"key":"4_CR74","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: On the decidability and complexity of metric temporal logic over finite words. Log. Methods Comput. Sci. 3(1) (2007)","DOI":"10.2168\/LMCS-3(1:8)2007"},{"key":"4_CR75","unstructured":"Pesic, M.: Constraint-based workflow management systems: shifting control to users. Ph.D. thesis, Technische Universiteit Eindhoven (2008)"},{"key":"4_CR76","doi-asserted-by":"crossref","unstructured":"Pesic, M., Schonenberg, H., van der Aalst, W.M.P.: DECLARE: full support for loosely-structured processes. In: EDOC, pp. 287\u2013300 (2007)","DOI":"10.1109\/EDOC.2007.14"},{"key":"4_CR77","doi-asserted-by":"crossref","unstructured":"Pesic, M., Schonenberg, H., van der Aalst, W.M.P.: DECLARE: full support for loosely-structured processes. In: EDOC, pp. 287\u2013300. IEEE Computer Society (2007)","DOI":"10.1109\/EDOC.2007.14"},{"key":"4_CR78","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/11837862_18","volume-title":"Business Process Management Workshops","author":"M Pesic","year":"2006","unstructured":"Pesic, M., van der Aalst, W.M.P.: A declarative approach for flexible business processes management. In: Eder, J., Dustdar, S. (eds.) BPM 2006. LNCS, vol. 4103, pp. 169\u2013180. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11837862_18"},{"key":"4_CR79","unstructured":"Pill, I., Quaritsch, T.: Behavioral diagnosis of LTL specifications at operator level. In: Rossi, F. (ed.) Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI 2013), pp. 1053\u20131059. IJCAI\/AAAI (2013)"},{"key":"4_CR80","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"2","key":"4_CR81","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1147\/rd.32.0114","volume":"3","author":"MO Rabin","year":"1959","unstructured":"Rabin, M.O., Scott, D.S.: Finite automata and their decision problems. IBM J. Res. Dev. 3(2), 114\u2013125 (1959)","journal-title":"IBM J. Res. Dev."},{"key":"4_CR82","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-030-99524-9_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Raha","year":"2022","unstructured":"Raha, R., Roy, R., Fijalkow, N., Neider, D.: Scalable anytime algorithms for learning fragments of linear temporal logic. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 263\u2013280. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_14"},{"key":"4_CR83","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30409-5","volume-title":"Enabling Flexibility in Process-Aware Information Systems - Challenges, Methods, Technologies","author":"M Reichert","year":"2012","unstructured":"Reichert, M., Weber, B.: Enabling Flexibility in Process-Aware Information Systems - Challenges, Methods, Technologies. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-30409-5"},{"key":"4_CR84","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23059-2","volume-title":"Business Process Management","year":"2011","unstructured":"Rinderle-Ma, S., Toumani, F., Wolf, K. (eds.): Business Process Management. LNCS, vol. 6896. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23059-2"},{"key":"4_CR85","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/3-540-45581-7_38","volume-title":"Conceptual Modeling \u2014 ER 2001","author":"S Sadiq","year":"2001","unstructured":"Sadiq, S., Sadiq, W., Orlowska, M.: Pockets of flexibility in workflow specification. In: S.Kunii, H., Jajodia, S., S\u00f8lvberg, A. (eds.) ER 2001. LNCS, vol. 2224, pp. 513\u2013526. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45581-7_38"},{"key":"4_CR86","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-319-46295-0_6","volume-title":"Service-Oriented Computing","author":"S Sch\u00f6nig","year":"2016","unstructured":"Sch\u00f6nig, S., Di Ciccio, C., Maggi, F.M., Mendling, J.: Discovery of multi-perspective declarative process models. In: Sheng, Q.Z., Stroulia, E., Tata, S., Bhiri, S. (eds.) ICSOC 2016. LNCS, vol. 9936, pp. 87\u2013103. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46295-0_6"},{"key":"4_CR87","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-319-93931-5_14","volume-title":"Business Information Systems","author":"DMM Schunselaar","year":"2018","unstructured":"Schunselaar, D.M.M., Slaats, T., Maggi, F.M., Reijers, H.A., van der Aalst, W.M.P.: Mining hybrid business process models: a quest for better precision. In: Abramowicz, W., Paschke, A. (eds.) BIS 2018. LNBIP, vol. 320, pp. 190\u2013205. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-93931-5_14"},{"key":"4_CR88","doi-asserted-by":"crossref","unstructured":"Singh, M.P.: Distributed enactment of multiagent workflows: temporal logic for web service composition. In: AAMAS, pp. 907\u2013914. ACM (2003)","DOI":"10.1145\/860575.860721"},{"key":"4_CR89","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-030-85469-0_6","volume-title":"Business Process Management","author":"T Slaats","year":"2021","unstructured":"Slaats, T., Debois, S., Back, C.O.: Weighing the pros and cons: process discovery with negative examples. In: Polyvyanyy, A., Wynn, M.T., Van Looy, A., Reichert, M. (eds.) BPM 2021. LNCS, vol. 12875, pp. 47\u201364. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85469-0_6"},{"key":"4_CR90","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/978-3-319-48472-3_32","volume-title":"On the Move to Meaningful Internet Systems: OTM 2016 Conferences","author":"T Slaats","year":"2016","unstructured":"Slaats, T., Schunselaar, D.M.M., Maggi, F.M., Reijers, H.A.: The semantics of hybrid process models. In: Debruyne, C., et al. (eds.) OTM 2016. LNCS, vol. 10033, pp. 531\u2013551. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48472-3_32"},{"key":"4_CR91","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-662-45391-9_10","volume-title":"Service-Oriented Computing","author":"Y Sun","year":"2014","unstructured":"Sun, Y., Su, J.: Conformance for DecSerFlow constraints. In: Franch, X., Ghose, A.K., Lewis, G.A., Bhiri, S. (eds.) ICSOC 2014. LNCS, vol. 8831, pp. 139\u2013153. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-45391-9_10"},{"key":"4_CR92","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49851-4","volume-title":"Process Mining - Data Science in Action","author":"WMP van der Aalst","year":"2016","unstructured":"van der Aalst, W.M.P.: Process Mining - Data Science in Action, 2nd edn. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49851-4","edition":"2"},{"key":"4_CR93","unstructured":"van der Aalst, W.M.P., Artale, A., Montali, M., Tritini, S.: Object-centric behavioral constraints: integrating data and declarative process modelling. In: Artale, A., Glimm, B., Kontchakov, R. (eds.) DL. CEUR Workshop Proceedings, vol. 1879. CEUR-WS.org (2017)"},{"key":"4_CR94","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11841197_1","volume-title":"Web Services and Formal Methods","author":"WMP van der Aalst","year":"2006","unstructured":"van der Aalst, W.M.P., Pesic, M.: DecSerFlow: towards a truly declarative service flow language. In: Bravetti, M., N\u00fa\u00f1ez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, pp. 1\u201323. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11841197_1"},{"key":"4_CR95","doi-asserted-by":"publisher","first-page":"101685","DOI":"10.1016\/j.is.2020.101685","volume":"102","author":"BF van Dongen","year":"2021","unstructured":"van Dongen, B.F., De Smedt, J., Di Ciccio, C., Mendling, J.: Conformance checking of mixed-paradigm process models. Inf. Syst. 102, 101685 (2021)","journal-title":"Inf. Syst."},{"key":"4_CR96","unstructured":"van Dongen, B.F., Montali, M., Wynn, M.T. (eds.) 2nd International Conference on Process Mining, ICPM 2020, Padua, Italy, 4\u20139 October 2020. IEEE (2020)"},{"key":"4_CR97","doi-asserted-by":"crossref","unstructured":"Westergaard, M.: Better algorithms for analyzing and enacting declarative workflow languages using LTL. In: Rinderle-Ma et al. [81], pp. 83\u201398","DOI":"10.1007\/978-3-642-23059-2_10"},{"key":"4_CR98","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-642-33606-5_16","volume-title":"On the Move to Meaningful Internet Systems: OTM 2012","author":"M Westergaard","year":"2012","unstructured":"Westergaard, M., Maggi, F.M.: Looking into the future. In: Meersman, R., et al. (eds.) OTM 2012. LNCS, vol. 7565, pp. 250\u2013267. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33606-5_16"},{"key":"4_CR99","doi-asserted-by":"crossref","unstructured":"Zhu, S., Tabajara, L.M., Pu, G., Vardi, M.Y.: On the power of automata minimization in temporal synthesis. In: Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2021). EPTCS, vol. 346, pp. 117\u2013134 (2021)","DOI":"10.4204\/EPTCS.346.8"}],"container-title":["Lecture Notes in Business Information Processing","Process Mining Handbook"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-08848-3_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,7]],"date-time":"2024-03-07T15:28:40Z","timestamp":1709825320000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-08848-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031088476","9783031088483"],"references-count":99,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-08848-3_4","relation":{},"ISSN":["1865-1348","1865-1356"],"issn-type":[{"value":"1865-1348","type":"print"},{"value":"1865-1356","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"27 June 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}