{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T21:08:12Z","timestamp":1757624892465,"version":"3.44.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783032029287"},{"type":"electronic","value":"9783032029294"}],"license":[{"start":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T00:00:00Z","timestamp":1756252800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T00:00:00Z","timestamp":1756252800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-02929-4_1","type":"book-chapter","created":{"date-parts":[[2025,8,26]],"date-time":"2025-08-26T10:14:35Z","timestamp":1756203275000},"page":"3-22","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["From Sound Workflow Nets to\u00a0LTL$$_f$$ Declarative Specifications by\u00a0Casting Three Spells"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2975-5330","authenticated-orcid":false,"given":"Luca","family":"Barbaro","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5466-9012","authenticated-orcid":false,"given":"Giovanni","family":"Varricchione","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8021-3430","authenticated-orcid":false,"given":"Marco","family":"Montali","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0955-6940","authenticated-orcid":false,"given":"Claudio","family":"Di Ciccio","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,8,27]]},"reference":[{"key":"1_CR1","unstructured":"van\u00a0der Aalst, W.M.P.: Structural characterizations of sound workflow nets, Technical report, 9623, Technische Universiteit Eindhoven (1996)"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"van\u00a0der Aalst, W.M.P.: Verification of workflow nets. In: ICATPN, pp. 407\u2013426 (1997)","DOI":"10.1007\/3-540-63139-9_48"},{"issue":"1","key":"1_CR3","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1142\/S0218126698000043","volume":"8","author":"WMP van der Aalst","year":"1998","unstructured":"van der Aalst, W.M.P.: The application of petri nets to workflow management. J. Circ. Syst. Comput. 8(1), 21\u201366 (1998)","journal-title":"J. Circ. Syst. Comput."},{"issue":"9","key":"1_CR4","doi-asserted-by":"publisher","first-page":"1128","DOI":"10.1109\/TKDE.2004.47","volume":"16","author":"WMP van der Aalst","year":"2004","unstructured":"van der Aalst, W.M.P., Weijters, T., Maruster, L.: Workflow mining: discovering process models from event logs. IEEE Trans. Knowl. Data Eng. 16(9), 1128\u20131142 (2004)","journal-title":"IEEE Trans. Knowl. Data Eng."},{"issue":"4","key":"1_CR5","doi-asserted-by":"publisher","first-page":"686","DOI":"10.1109\/TKDE.2018.2841877","volume":"31","author":"A Augusto","year":"2019","unstructured":"Augusto, A., Conforti, R., Dumas, M., La Rosa, M., Maggi, F.M., Marella, A.: Automated discovery of process models from event logs: review and benchmark. IEEE Trans. Knowl. Data Eng. 31(4), 686\u2013705 (2019)","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Baumann, M.: Comparing imperative and declarative process models with flow dependencies. In: IEEESOSE 2018, pp. 63\u201368. IEEE Computer Society (2018)","DOI":"10.1109\/SOSE.2018.00017"},{"key":"1_CR7","unstructured":"Bergmann, A., Rebmann, A., Kampik, T.: BPMN2Constraints: breaking down BPMN diagrams into declarative process query constraints. In: BPM Demos, vol.\u00a03469, pp. 137\u2013141 (2023)"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Busch, K., Kampik, T., Leopold, H.: xSemAD: explainable semantic anomaly detection in event logs using sequence-to-sequence models. In: BPM, vol. 14940, pp. 309\u2013327 (2024)","DOI":"10.1007\/978-3-031-70396-6_18"},{"key":"1_CR9","doi-asserted-by":"publisher","first-page":"102312","DOI":"10.1016\/j.is.2023.102312","volume":"120","author":"A Cecconi","year":"2024","unstructured":"Cecconi, A., Barbaro, L., Ciccio, C.D., Senderovich, A.: Measuring rule-based LTLf process specifications: a probabilistic data-driven approach. Inf. Syst. 120, 102312 (2024)","journal-title":"Inf. Syst."},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Cecconi, A., Di\u00a0Ciccio, C., De\u00a0Giacomo, G., Mendling, J.: Interestingness of traces in declarative process mining: the Janus LTLpf approach. In: BPM, pp. 121\u2013138 (2018)","DOI":"10.1007\/978-3-319-98648-7_8"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Cosma, V.P., Hildebrandt, T.T., Slaats, T.: Transforming dynamic condition response graphs to safe petri nets. In: PETRI NETS 2023. LNCS, vol. 13929, pp. 417\u2013439. Springer (2023)","DOI":"10.1007\/978-3-031-33620-1_22"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"De\u00a0Giacomo, G., De\u00a0Masellis, R., Montali, M.: Reasoning on LTL on finite traces: insensitivity to infiniteness. In: AAAI, pp. 1027\u20131033 (2014)","DOI":"10.1609\/aaai.v28i1.8872"},{"key":"1_CR13","unstructured":"De\u00a0Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: IJCAI, pp. 854\u2013860 (2013)"},{"issue":"1","key":"1_CR14","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":"1_CR15","doi-asserted-by":"crossref","unstructured":"Desel, J., Reisig, W.: Place\/transition Petri Nets, pp. 122\u2013173 (1998)","DOI":"10.1007\/3-540-65306-6_15"},{"key":"1_CR16","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1016\/j.is.2015.06.009","volume":"56","author":"C Di Ciccio","year":"2016","unstructured":"Di Ciccio, C., Maggi, F.M., Mendling, J.: Efficient discovery of target-branched declare constraints. Inf. Syst. 56, 258\u2013283 (2016)","journal-title":"Inf. Syst."},{"key":"1_CR17","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":"1_CR18","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/j.is.2018.01.011","volume":"78","author":"C Di Ciccio","year":"2018","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)","journal-title":"Inf. Syst."},{"key":"1_CR19","doi-asserted-by":"publisher","unstructured":"Di\u00a0Ciccio, C., Montali, M.: Declarative process specifications: reasoning, discovery, monitoring. In: van der Aalst, W.M.P., Carmona, J. (eds.) Process Mining Handbook. Lecture Notes in Business Information Processing, vol. 448, pp. 108\u2013152. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-08848-3_4","DOI":"10.1007\/978-3-031-08848-3_4"},{"key":"1_CR20","unstructured":"van Dongen, B.: BPI challenge 2015 municipality 5 (2015)"},{"key":"1_CR21","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":"1_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-56509-4","volume-title":"Fundamentals of Business Process Management","author":"M Dumas","year":"2018","unstructured":"Dumas, M., La Rosa, M., Mendling, J., Reijers, H.: Fundamentals of Business Process Management, 2nd edn. Springer, Berlin, Heidelberg (2018)","edition":"2"},{"issue":"9","key":"1_CR23","doi-asserted-by":"publisher","first-page":"1031","DOI":"10.1016\/j.ic.2010.05.002","volume":"208","author":"D Gorla","year":"2010","unstructured":"Gorla, D.: Towards a unified approach to encodability and separation results for process calculi. Inf. Comput. 208(9), 1031\u20131053 (2010)","journal-title":"Inf. Comput."},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Hildebrandt, T.T., Mukkamala, R.R.: Declarative event-based workflow as distributed dynamic condition response graphs. In: PLACES 2010, vol.\u00a069, pp. 59\u201373 (2010)","DOI":"10.4204\/EPTCS.69.5"},{"key":"1_CR25","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, Boston, MA, USA (2006)","edition":"3"},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Leemans, S.J.J., Fahland, D., van\u00a0der Aalst, W.M.P.: Discovering block-structured process models from event logs containing infrequent behaviour. In: BPM Workshops 2013, vol.\u00a0171, pp. 66\u201378 (2013)","DOI":"10.1007\/978-3-319-06257-0_6"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A., Zuck, L.D.: The glory of the past. In: Logics of Programs, pp. 196\u2013218 (1985)","DOI":"10.1007\/3-540-15648-8_16"},{"issue":"1","key":"1_CR28","doi-asserted-by":"publisher","first-page":"2:1","DOI":"10.1145\/1555392.1555395","volume":"19","author":"C Ouyang","year":"2009","unstructured":"Ouyang, C., Dumas, M., van der Aalst, W.M.P., Ter Hofstede, A.H.M., Mendling, J.: From business process models to process-oriented software systems. ACM Trans. Softw. Eng. Methodol. 19(1), 2:1-2:37 (2009)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"1_CR29","unstructured":"Pesic, M.: Constraint-based workflow management systems: shifting control to users, Ph.D. thesis, TU Eindhoven (2008)"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Pichler, P., Weber, B., Zugal, S., Pinggera, J., Mendling, J., Reijers, H.A.: Imperative versus declarative process modeling languages: an empirical investigation. In: BPM Workshops 2011, vol.\u00a099, pp. 383\u2013394 (2011)","DOI":"10.1007\/978-3-642-28108-2_37"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"1_CR32","unstructured":"Prescher, J., Di Ciccio, C., Mendling, J.: From declarative processes to imperative models. In: SIMPDA 2014, vol.\u00a01293, pp. 162\u2013173 (2014)"},{"key":"1_CR33","unstructured":"Rebmann, A., Kampik, T., Corea, C., van\u00a0der Aa, H.: Mining constraints from reference process models for detecting best-practice violations in event log. arXiv preprint arXiv:2407.02336 (2024)"},{"key":"1_CR34","doi-asserted-by":"crossref","unstructured":"Rocha, E.G., van Zelst, S.J., van\u00a0der Aalst, W.M.P.: Mining behavioral patterns for conformance diagnostics. In: BPM 2024, vol. 14940, pp. 291\u2013308 (2024)","DOI":"10.1007\/978-3-031-70396-6_17"}],"container-title":["Lecture Notes in Business Information Processing","Business Process Management Forum"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-02929-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,9]],"date-time":"2025-09-09T16:24:57Z","timestamp":1757435097000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-02929-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,27]]},"ISBN":["9783032029287","9783032029294"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-02929-4_1","relation":{},"ISSN":["1865-1348","1865-1356"],"issn-type":[{"type":"print","value":"1865-1348"},{"type":"electronic","value":"1865-1356"}],"subject":[],"published":{"date-parts":[[2025,8,27]]},"assertion":[{"value":"27 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"BPM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Business Process Management","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Seville","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 August 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"bpm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.bpm2025seville.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}