{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,8]],"date-time":"2024-07-08T21:24:15Z","timestamp":1720473855204},"reference-count":61,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2023,3,1]],"date-time":"2023-03-01T00:00:00Z","timestamp":1677628800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2023,3,1]],"date-time":"2023-03-01T00:00:00Z","timestamp":1677628800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2023,3,1]],"date-time":"2023-03-01T00:00:00Z","timestamp":1677628800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2023,3,1]],"date-time":"2023-03-01T00:00:00Z","timestamp":1677628800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2023,3,1]],"date-time":"2023-03-01T00:00:00Z","timestamp":1677628800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,3,1]],"date-time":"2023-03-01T00:00:00Z","timestamp":1677628800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Information Systems"],"published-print":{"date-parts":[[2023,3]]},"DOI":"10.1016\/j.is.2022.102157","type":"journal-article","created":{"date-parts":[[2022,12,9]],"date-time":"2022-12-09T11:14:47Z","timestamp":1670584487000},"page":"102157","update-policy":"http:\/\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Reduction of data-value-aware process models: A relevance-based approach"],"prefix":"10.1016","volume":"114","author":[{"ORCID":"http:\/\/orcid.org\/0000-0002-5680-8346","authenticated-orcid":false,"given":"Elaheh","family":"Ordoni","sequence":"first","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0002-5515-7756","authenticated-orcid":false,"given":"Jutta","family":"M\u00fclle","sequence":"additional","affiliation":[]},{"given":"Klemens","family":"B\u00f6hm","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.is.2022.102157_b1","series-title":"Principles of Model Checking","author":"Baier","year":"2008"},{"key":"10.1016\/j.is.2022.102157_b2","series-title":"Handbook of Spectrum Auction Design","author":"Bichler","year":"2017"},{"key":"10.1016\/j.is.2022.102157_b3","series-title":"Verifying Workflow Models with Data Values: A Case Study of SMR Spectrum Auctions","author":"Ordoni","year":"2019"},{"key":"10.1016\/j.is.2022.102157_b4","series-title":"International Conference on Business Process Management","first-page":"494","article-title":"Compliance checking for decision-aware process models","author":"Haarmann","year":"2018"},{"key":"10.1016\/j.is.2022.102157_b5","series-title":"Model Checking","author":"Clarke","year":"2018"},{"key":"10.1016\/j.is.2022.102157_b6","series-title":"International Conference on Application and Theory of Petri Nets","first-page":"46","article-title":"Stubborn sets for standard properties","author":"Schmidt","year":"1999"},{"key":"10.1016\/j.is.2022.102157_b7","series-title":"International Conference on Conceptual Modeling","first-page":"332","article-title":"On enabling data-aware compliance checking of business process models","author":"Knuplesch","year":"2010"},{"key":"10.1016\/j.is.2022.102157_b8","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1016\/j.is.2014.07.001","article-title":"A new verification technique for large processes based on identification of relevant tasks","volume":"47","author":"Mrasek","year":"2015","journal-title":"Inf. Syst."},{"key":"10.1016\/j.is.2022.102157_b9","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1016\/j.is.2018.12.002","article-title":"A practical data-flow verification scheme for business processes","volume":"81","author":"M\u00fclle","year":"2019","journal-title":"Inf. Syst."},{"key":"10.1016\/j.is.2022.102157_b10","series-title":"International Conference on Conceptual Modeling","first-page":"121","article-title":"Deciding data object relevance for business process model abstraction","author":"Harzmann","year":"2013"},{"key":"10.1016\/j.is.2022.102157_b11","series-title":"International Conference on Business Process Management","first-page":"55","article-title":"Petri nets with parameterised data","author":"Ghilardi","year":"2020"},{"key":"10.1016\/j.is.2022.102157_b12","doi-asserted-by":"crossref","first-page":"F305","DOI":"10.1111\/ecoj.12406","article-title":"The German 4G spectrum auction: Design and behaviour","author":"Cramton","year":"2017","journal-title":"Econ. J. 127"},{"issue":"1","key":"10.1016\/j.is.2022.102157_b13","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1257\/mic.2.1.39","article-title":"An experimental test of flexible combinatorial spectrum auction formats","volume":"2","author":"Brunner","year":"2010","journal-title":"Am. Econ. J. Microecon."},{"key":"10.1016\/j.is.2022.102157_b14","series-title":"Formal Models and Semantics","first-page":"995","article-title":"Temporal and modal logic","author":"Emerson","year":"1990"},{"key":"10.1016\/j.is.2022.102157_b15","series-title":"Logic in Computer Science: Modelling and Reasoning About Systems","author":"Huth","year":"2004"},{"key":"10.1016\/j.is.2022.102157_b16","series-title":"International Conference on Advanced Information Systems Engineering","first-page":"431","article-title":"On structured workflow modelling","author":"Kiepuszewski","year":"2000"},{"key":"10.1016\/j.is.2022.102157_b17","series-title":"OTM Confederated International Conferences\u201c on the Move to Meaningful Internet Systems\u201d","first-page":"121","article-title":"Untangling unstructured cyclic flows\u2013A solution based on continuations","author":"Koehler","year":"2004"},{"issue":"6","key":"10.1016\/j.is.2022.102157_b18","doi-asserted-by":"crossref","first-page":"518","DOI":"10.1016\/j.is.2011.10.005","article-title":"Structuring acyclic process models","volume":"37","author":"Polyvyanyy","year":"2012","journal-title":"Inf. Syst."},{"key":"10.1016\/j.is.2022.102157_b19","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/j.datak.2015.10.003","article-title":"Converting unstructured into semi-structured process models","volume":"101","author":"Eshuis","year":"2016","journal-title":"Data Knowl. Eng."},{"key":"10.1016\/j.is.2022.102157_b20","series-title":"International Workshop on Web Services and Formal Methods","first-page":"25","article-title":"Simplified computation and generalization of the refined process structure tree","author":"Polyvyanyy","year":"2010"},{"issue":"3\u20134","key":"10.1016\/j.is.2022.102157_b21","first-page":"399","article-title":"Causal behavioural profiles\u2013efficient computation, applications, and evaluation","volume":"113","author":"Weidlich","year":"2011","journal-title":"Fund. Inform."},{"key":"10.1016\/j.is.2022.102157_b22","series-title":"International Conference on Logic Programming","first-page":"440","article-title":"Verification from declarative specifications using logic programming","author":"Montali","year":"2008"},{"issue":"12","key":"10.1016\/j.is.2022.102157_b23","doi-asserted-by":"crossref","first-page":"1281","DOI":"10.1016\/j.infsof.2008.02.006","article-title":"Semantics and analysis of business process models in BPMN","volume":"50","author":"Dijkman","year":"2008","journal-title":"Inf. Softw. Technol."},{"key":"10.1016\/j.is.2022.102157_b24","series-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","first-page":"690","article-title":"A generic framework for reasoning about dynamic networks of infinite-state processes","author":"Bouajjani","year":"2007"},{"issue":"3","key":"10.1016\/j.is.2022.102157_b25","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1507244.1507246","article-title":"LTL with the freeze quantifier and register automata","volume":"10","author":"Demri","year":"2009","journal-title":"ACM Trans. Comput. Logic (TOCL)"},{"issue":"3","key":"10.1016\/j.is.2022.102157_b26","first-page":"251","article-title":"Nets with tokens which carry data","volume":"88","author":"Lazi\u0107","year":"2008","journal-title":"Fund. Inform."},{"key":"10.1016\/j.is.2022.102157_b27","series-title":"International Conference on Applications and Theory of Petri Nets and Concurrency","first-page":"20","article-title":"Decidability border for Petri nets with data: WQO dichotomy conjecture","author":"Lasota","year":"2016"},{"key":"10.1016\/j.is.2022.102157_b28","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1016\/j.ic.2017.08.007","article-title":"First-order \u03bc-calculus over generic transition systems and applications to the situation calculus","volume":"259","author":"Calvanese","year":"2018","journal-title":"Inform. and Comput."},{"key":"10.1016\/j.is.2022.102157_b29","series-title":"International Conference on Formal Methods in Computer-Aided Design","first-page":"127","article-title":"Checking safety properties using induction and a SAT-solver","author":"Sheeran","year":"2000"},{"key":"10.1016\/j.is.2022.102157_b30","series-title":"International Workshop on Verification, Model Checking, and Abstract Interpretation","first-page":"70","article-title":"SAT-based model checking without unrolling","author":"Bradley","year":"2011"},{"key":"10.1016\/j.is.2022.102157_b31","article-title":"Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis","volume":"6","author":"Ranise","year":"2010","journal-title":"Log. Methods Comput. Sci."},{"key":"10.1016\/j.is.2022.102157_b32","series-title":"International Conference on Computer Aided Verification","first-page":"334","article-title":"The nuXmv symbolic model checker","author":"Cavada","year":"2014"},{"key":"10.1016\/j.is.2022.102157_b33","series-title":"International Conference on Computer Aided Verification","first-page":"510","article-title":"The kind 2 model checker","author":"Champion","year":"2016"},{"key":"10.1016\/j.is.2022.102157_b34","series-title":"International Joint Conference on Automated Reasoning","first-page":"22","article-title":"MCMT: A model checker modulo theories","author":"Ghilardi","year":"2010"},{"issue":"537","key":"10.1016\/j.is.2022.102157_b35","doi-asserted-by":"crossref","first-page":"855","DOI":"10.1111\/j.1468-0297.2009.02249.x","article-title":"Bidding behaviour in multi-unit auctions\u2013An experimental investigation","volume":"119","author":"Engelmann","year":"2009","journal-title":"Econ. J."},{"key":"10.1016\/j.is.2022.102157_b36","series-title":"The Swiss UMTS spectrum auction flop: Bad luck or bad design?","author":"Wolfstetter","year":"2001"},{"key":"10.1016\/j.is.2022.102157_b37","series-title":"Putting Auction Theory to Work","author":"Milgrom","year":"2004"},{"issue":"3","key":"10.1016\/j.is.2022.102157_b38","doi-asserted-by":"crossref","first-page":"461","DOI":"10.1111\/joes.12017","article-title":"Multiunit auctions","volume":"27","author":"Kwasnica","year":"2013","journal-title":"J. Econ. Surv."},{"key":"10.1016\/j.is.2022.102157_b39","series-title":"International Conference on Application and Theory of Petri Nets","first-page":"465","article-title":"Lola a low level analyser","author":"Schmidt","year":"2000"},{"key":"10.1016\/j.is.2022.102157_b40","series-title":"International Conference on Business Process Management","first-page":"5","article-title":"Diagnosing and repairing data anomalies in process models","author":"Awad","year":"2009"},{"key":"10.1016\/j.is.2022.102157_b41","series-title":"International Conference on Conceptual Modeling","first-page":"219","article-title":"A holistic approach for soundness verification of decision-aware process models","author":"Leoni","year":"2018"},{"key":"10.1016\/j.is.2022.102157_b42","series-title":"2019 19th International Conference on Application of Concurrency to System Design","first-page":"82","article-title":"Soundness verification of decision-aware process models with variable-to-variable conditions","author":"Felli","year":"2019"},{"key":"10.1016\/j.is.2022.102157_b43","series-title":"International Conference on Advanced Information Systems Engineering","first-page":"389","article-title":"Soundness of data-aware processes with arithmetic conditions","author":"Felli","year":"2022"},{"key":"10.1016\/j.is.2022.102157_b44","series-title":"Transactions on Petri Nets and Other Models of Concurrency XII","first-page":"91","article-title":"Db-Nets: On the marriage of colored Petri nets and relational databases","author":"Montali","year":"2017"},{"key":"10.1016\/j.is.2022.102157_b45","series-title":"International Conference on Business Process Management","first-page":"157","article-title":"Formal modeling and SMT-based parameterized verification of data-aware BPMN","author":"Calvanese","year":"2019"},{"key":"10.1016\/j.is.2022.102157_b46","doi-asserted-by":"crossref","unstructured":"P. Felli, M. Montali, S. Winkler, Linear-time verification of data-aware dynamic systems with arithmetic, in: Proceedings of 36th AAAI, 2022.","DOI":"10.1007\/978-3-031-10769-6_4"},{"key":"10.1016\/j.is.2022.102157_b47","series-title":"Automated Reasoning","first-page":"36","article-title":"CTL\u2217 model checking for data-aware dynamic systems with arithmetic","author":"Felli","year":"2022"},{"key":"10.1016\/j.is.2022.102157_b48","series-title":"International Conference on Advanced Information Systems Engineering","first-page":"497","article-title":"A semantic approach for business process model abstraction","author":"Smirnov","year":"2011"},{"issue":"1","key":"10.1016\/j.is.2022.102157_b49","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/s10619-011-7088-5","article-title":"Business process model abstraction: A definition, catalog, and survey","volume":"30","author":"Smirnov","year":"2012","journal-title":"Distrib. Parallel Databases"},{"key":"10.1016\/j.is.2022.102157_b50","series-title":"International Conference on Conceptual Modeling","first-page":"292","article-title":"Data support in process model abstraction","author":"Meyer","year":"2012"},{"key":"10.1016\/j.is.2022.102157_b51","series-title":"International Conference on Business Process Management","first-page":"88","article-title":"View-based process visualization","author":"Bobrik","year":"2007"},{"key":"10.1016\/j.is.2022.102157_b52","series-title":"Handbook on Business Process Management, Vol. 1","first-page":"147","article-title":"Business process model abstraction","author":"Polyvyanyy","year":"2015"},{"key":"10.1016\/j.is.2022.102157_b53","doi-asserted-by":"crossref","unstructured":"C. Tsagkani, A. Tsalgatidou, Abstracting BPMN models, in: Proceedings of the 19th Panhellenic Conference on Informatics, 2015, pp. 243\u2013244.","DOI":"10.1145\/2801948.2802035"},{"issue":"11","key":"10.1016\/j.is.2022.102157_b54","doi-asserted-by":"crossref","first-page":"2322","DOI":"10.3390\/app9112322","article-title":"A pattern based method for simplifying a BPMN process model","volume":"9","author":"Ramos-Merino","year":"2019","journal-title":"Appl. Sci."},{"issue":"2","key":"10.1016\/j.is.2022.102157_b55","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1050849.1050865","article-title":"A brief survey of program slicing","volume":"30","author":"Xu","year":"2005","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"10.1016\/j.is.2022.102157_b56","series-title":"International Conference on Computer Aided Verification","first-page":"72","article-title":"Construction of abstract state graphs with PVS","author":"Graf","year":"1997"},{"key":"10.1016\/j.is.2022.102157_b57","doi-asserted-by":"crossref","unstructured":"W. Visser, S. Park, J. Penix, Using predicate abstraction to reduce object-oriented programs for model checking, in: Proceedings of the Third Workshop on Formal Methods in Software Practice, 2000, pp. 3\u2013182.","DOI":"10.1145\/349360.351125"},{"issue":"2","key":"10.1016\/j.is.2022.102157_b58","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1006\/inco.1998.2778","article-title":"A partial order approach to branching time logic model checking","volume":"150","author":"Gerth","year":"1999","journal-title":"Inform. and Comput."},{"issue":"1\u20134","key":"10.1016\/j.is.2022.102157_b59","first-page":"331","article-title":"Stubborn sets for model checking the EF\/AG fragment of CTL","volume":"43","author":"Schmidt","year":"2000","journal-title":"Fund. Inform."},{"issue":"01","key":"10.1016\/j.is.2022.102157_b60","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1142\/S0218126698000043","article-title":"The application of Petri nets to workflow management","volume":"8","author":"Van der Aalst","year":"1998","journal-title":"J. Circuits Syst. Comput."},{"issue":"9","key":"10.1016\/j.is.2022.102157_b61","doi-asserted-by":"crossref","first-page":"793","DOI":"10.1016\/j.datak.2009.02.015","article-title":"The refined process structure tree","volume":"68","author":"Vanhatalo","year":"2009","journal-title":"Data Knowl. Eng."}],"container-title":["Information Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0306437922001351?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0306437922001351?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2023,9,20]],"date-time":"2023-09-20T11:31:00Z","timestamp":1695209460000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0306437922001351"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,3]]},"references-count":61,"alternative-id":["S0306437922001351"],"URL":"https:\/\/doi.org\/10.1016\/j.is.2022.102157","relation":{},"ISSN":["0306-4379"],"issn-type":[{"value":"0306-4379","type":"print"}],"subject":[],"published":{"date-parts":[[2023,3]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Reduction of data-value-aware process models: A relevance-based approach","name":"articletitle","label":"Article Title"},{"value":"Information Systems","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.is.2022.102157","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2022 Elsevier Ltd. All rights reserved.","name":"copyright","label":"Copyright"}],"article-number":"102157"}}