{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,8]],"date-time":"2026-02-08T05:31:43Z","timestamp":1770528703005,"version":"3.49.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319453477","type":"print"},{"value":"9783319453484","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-45348-4_10","type":"book-chapter","created":{"date-parts":[[2016,9,7]],"date-time":"2016-09-07T16:06:15Z","timestamp":1473264375000},"page":"158-175","source":"Crossref","is-referenced-by-count":10,"title":["Semantical Vacuity Detection in Declarative Process Mining"],"prefix":"10.1007","author":[{"given":"Fabrizio Maria","family":"Maggi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Montali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claudio","family":"Di Ciccio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Mendling","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,9,8]]},"reference":[{"key":"10_CR1","first-page":"99","volume":"23","author":"W Aalst van der","year":"2009","unstructured":"van der Aalst, W., Pesic, M., Schonenberg, H.: Declarative workflows: balancing between flexibility and support. Comput. Sci. - R&D 23, 99\u2013113 (2009)","journal-title":"Comput. Sci. - R&D"},{"issue":"4","key":"10_CR2","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14 (2011)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"2","key":"10_CR3","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1023\/A:1008779610539","volume":"18","author":"I Beer","year":"2001","unstructured":"Beer, I., Eisner, C.: Efficient detection of vacuity in temporal model checking. Formal Meth. Syst. Des. 18(2), 141\u2013163 (2001)","journal-title":"Formal Meth. Syst. Des."},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Burattin, A., Maggi, F.M., van der Aalst, W.M.P., Sperduti, A.: Techniques for a posteriori analysis of declarative processes. In: Proceedings of EDOC. IEEE (2012)","DOI":"10.1109\/EDOC.2012.15"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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 Alast, W.M.P. (eds.) Transactions on Petri Nets and Other Models of Concurrency II. LNCS, vol. 5460, pp. 278\u2013295. Springer, Heidelberg (2009)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-642-23059-2_3","volume-title":"Business Process Management","author":"E Damaggio","year":"2011","unstructured":"Damaggio, E., Deutsch, A., Hull, R., Vianu, V.: Automatic verification of data-centric business processes. In: Rinderle-Ma, S., Toumani, F., Wolf, K. (eds.) BPM 2011. LNCS, vol. 6896, pp. 3\u201316. Springer, Heidelberg (2011)"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-319-10172-9_1","volume-title":"Business Process Management","author":"G Giacomo De","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, Heidelberg (2014)"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"De Giacomo, G., De Masellis, R., Montali, M.: Reasoning on LTL on finite traces: insensitivity to infiniteness. In: Proceedings of AAAI (2014)","DOI":"10.1609\/aaai.v28i1.8872"},{"key":"10_CR9","unstructured":"De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of IJCAI. AAAI (2013)"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"De Masellis, R., Maggi, F.M., Montali, M.: Monitoring data-aware business constraints with finite state automata. In: Proceedings of ICSSP. ACM (2014)","DOI":"10.1145\/2600821.2600835"},{"key":"10_CR11","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1016\/j.is.2015.06.009","volume":"56","author":"C Ciccio Di","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":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1007\/978-3-319-23063-4_9","volume-title":"Business Process Management","author":"C Ciccio Di","year":"2015","unstructured":"Di Ciccio, C., Maggi, F.M., Montali, M., Mendling, J.: Ensuring model consistency in declarative process discovery. In: Motahari-Nezhad, H.R., Recker, J., Weidlich, M. (eds.) BPM 2015. LNCS, vol. 9253, pp. 144\u2013159. Springer, Heidelberg (2015)"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Di Ciccio, C., Mecella, M.: A two-step fast algorithm for the automated discovery of declarative workflows. In: Proceedings of CIDM. IEEE (2013)","DOI":"10.1109\/CIDM.2013.6597228"},{"issue":"4","key":"10_CR14","first-page":"24","volume":"5","author":"C Ciccio Di","year":"2015","unstructured":"Di Ciccio, C., Mecella, M.: On the discovery of declarative control flows for artful processes. ACM Trans. Manag. Inf. Syst. 5(4), 24 (2015)","journal-title":"ACM Trans. Manag. Inf. Syst."},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., Havelund, K.: Automata-based verification of temporal properties on running programs. In: Proceedings of ASE. IEEE (2001)","DOI":"10.1109\/ASE.2001.989841"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1007\/978-3-642-16373-9_24","volume-title":"Conceptual Modeling \u2013 ER 2010","author":"D Knuplesch","year":"2010","unstructured":"Knuplesch, D., Ly, L.T., Rinderle-Ma, S., Pfeifer, H., Dadam, P.: On enabling data-aware compliance checking of business process models. In: Parsons, J., Saeki, M., Shoval, P., Woo, C., Wand, Y. (eds.) ER 2010. LNCS, vol. 6412, pp. 332\u2013346. Springer, Heidelberg (2010)"},{"key":"10_CR17","doi-asserted-by":"crossref","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. Transf. 4, 224\u2013233 (2003)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"10_CR19","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1016\/j.is.2013.12.005","volume":"47","author":"M Leoni de","year":"2015","unstructured":"de Leoni, M., Maggi, F.M., van der Aalst, W.M.P.: 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."},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1007\/978-3-642-23059-2_13","volume-title":"Business Process Management","author":"FM Maggi","year":"2011","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, S., Toumani, F., Wolf, K. (eds.) BPM 2011. LNCS, vol. 6896, pp. 132\u2013147. Springer, Heidelberg (2011)"},{"key":"10_CR22","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: Proceedings of CIDM (2011)","DOI":"10.1109\/CIDM.2011.5949297"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"10_CR24","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/978-3-642-14538-4_2","volume-title":"Specification and Verification of Declarative Open Interaction Models","author":"M Montali","year":"2010","unstructured":"Montali, M.: Declarative open interaction models. In: Montali, M. (ed.) Specification and Verification of Declarative Open Interaction Models. LNBIP, vol. 56, pp. 11\u201345. Springer, Heidelberg (2010)"},{"issue":"1","key":"10_CR25","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1145\/2542182.2542199","volume":"5","author":"M Montali","year":"2013","unstructured":"Montali, M., Maggi, F.M., Chesani, F., Mello, P., van der Aalst, W.M.P.: Monitoring business constraints with the event calculus. ACM Trans. Intell. Syst. Technol. 5(1), 17 (2013)","journal-title":"ACM Trans. Intell. Syst. Technol."},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Pesic, M., Schonenberg, H., van der Aalst, W.: DECLARE: full support for loosely-structured processes. In: Proceedings of EDOC. IEEE (2007)","DOI":"10.1109\/EDOC.2007.14"},{"key":"10_CR27","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1007\/978-3-642-28108-2_37","volume-title":"Business Process Management Workshops","author":"P Pichler","year":"2012","unstructured":"Pichler, P., Weber, B., Zugal, S., Pinggera, J., Mendling, J., Reijers, H.A.: Imperative versus declarative process modeling languages: an empirical investigation. In: Daniel, F., Barkaoui, K., Dustdar, S. (eds.) BPM Workshops 2011, Part I. LNBIP, vol. 99, pp. 383\u2013394. Springer, Heidelberg (2012)"},{"key":"10_CR28","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/978-3-642-21759-3_12","volume-title":"Enterprise, Business-Process and Information Systems Modeling","author":"S Zugal","year":"2011","unstructured":"Zugal, S., Pinggera, J., Weber, B.: The impact of testcases on the maintainability of declarative process models. In: Halpin, T., Nurcan, S., Krogstie, J., Soffer, P., Proper, E., Schmidt, R., Bider, I. (eds.) BPMDS 2011 and EMMSAD 2011. LNBIP, vol. 81, pp. 163\u2013177. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Business Process Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-45348-4_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,7]],"date-time":"2022-07-07T22:01:16Z","timestamp":1657231276000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-45348-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319453477","9783319453484"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-45348-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}