{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:07:51Z","timestamp":1762459671730,"version":"3.41.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319998398"},{"type":"electronic","value":"9783319998404"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-99840-4_5","type":"book-chapter","created":{"date-parts":[[2018,9,7]],"date-time":"2018-09-07T11:29:08Z","timestamp":1536319748000},"page":"76-97","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Symbolic Specification and Verification of Data-Aware BPMN Processes Using Rewriting Modulo SMT"],"prefix":"10.1007","author":[{"given":"Francisco","family":"Dur\u00e1n","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Camilo","family":"Rocha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gwen","family":"Sala\u00fcn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,9,8]]},"reference":[{"key":"5_CR1","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1999","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1999)"},{"issue":"1\u20133","key":"5_CR2","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1016\/j.tcs.2006.04.012","volume":"360","author":"R Bruni","year":"2006","unstructured":"Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theor. Comput. Sci. 360(1\u20133), 386\u2013414 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-45348-4_13","volume-title":"Business Process Management","author":"D Calvanese","year":"2016","unstructured":"Calvanese, D., Dumas, M., Laurson, \u00dc., Maggi, F.M., Montali, M., Teinemaa, I.: Semantics and analysis of DMN decision tables. In: La Rosa, M., Loos, P., Pastor, O. (eds.) BPM 2016. LNCS, vol. 9850, pp. 217\u2013233. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-45348-4_13"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude - A High-Performance Logical Framework","author":"P Lincoln","year":"2007","unstructured":"Lincoln, P., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Corradini, F., Fornari, F., Polini, A., Re, B., Tiezzi, F., Vandin, A.: BProVe: a formal verification framework for business process models. In: Proceedings of ASE, pp. 217\u2013228. IEEE Computer Society (2017)","DOI":"10.1109\/ASE.2017.8115635"},{"issue":"2","key":"5_CR6","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1016\/j.is.2010.06.005","volume":"36","author":"G Decker","year":"2011","unstructured":"Decker, G., Weske, M.: Interaction-centric modeling of process choreographies. Inf. Syst. 36(2), 292\u2013312 (2011)","journal-title":"Inf. Syst."},{"issue":"12","key":"5_CR7","doi-asserted-by":"publisher","first-page":"1281","DOI":"10.1016\/j.infsof.2008.02.006","volume":"50","author":"R Dijkman","year":"2008","unstructured":"Dijkman, R., Dumas, M., Ouyang, C.: Semantics and analysis of business process models in BPMN. Inf. Softw. Technol. 50(12), 1281\u20131294 (2008)","journal-title":"Inf. Softw. Technol."},{"issue":"12","key":"5_CR8","doi-asserted-by":"publisher","first-page":"1281","DOI":"10.1016\/j.infsof.2008.02.006","volume":"50","author":"RM Dijkman","year":"2008","unstructured":"Dijkman, R.M., Dumas, M., Ouyang, C.: Semantics and analysis of business process models in BPMN. Inf. Softw. Technol. 50(12), 1281\u20131294 (2008)","journal-title":"Inf. Softw. Technol."},{"issue":"1\u20132","key":"5_CR9","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s10990-008-9028-2","volume":"21","author":"F Dur\u00e1n","year":"2008","unstructured":"Dur\u00e1n, F., Lucas, S., March\u00e9, C., Meseguer, J., Urbain, X.: Proving operational termination of membership equational programs. High. Order Symb. Comput. 21(1\u20132), 59\u201388 (2008)","journal-title":"High. Order Symb. Comput."},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-319-59746-1_12","volume-title":"Coordination Models and Languages","author":"F Dur\u00e1n","year":"2017","unstructured":"Dur\u00e1n, F., Sala\u00fcn, G.: Verifying timed BPMN processes using Maude. In: Jacquet, J.-M., Massink, M. (eds.) COORDINATION 2017. LNCS, vol. 10319, pp. 219\u2013236. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-59746-1_12"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"El-Saber, N., Boronat, A.: BPMN formalization and verification using Maude. In: Proceedings of BM-FA, pp. 1\u20138. ACM (2014)","DOI":"10.1145\/2630768.2630769"},{"issue":"2","key":"5_CR12","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","volume":"105","author":"JA Goguen","year":"1992","unstructured":"Goguen, J.A., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci. 105(2), 217\u2013273 (1992)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"5_CR13","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1109\/TSC.2015.2413401","volume":"9","author":"M G\u00fcdemann","year":"2016","unstructured":"G\u00fcdemann, M., Poizat, P., Sala\u00fcn, G., Ye, L.: VerChor: a framework for the design and verification of choreographies. IEEE Trans. Serv. Comput. 9(4), 647\u2013660 (2016)","journal-title":"IEEE Trans. Serv. Comput."},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Herbert, L., Sharp, R.: Using stochastic model checking to provision complex business services. In: Proceedings of HASE, pp. 98\u2013105. IEEE (2012)","DOI":"10.1109\/HASE.2012.29"},{"key":"5_CR15","unstructured":"ISO\/IEC: International Standard 19510, Information Technology - Business Process Model and Notation (2013)"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-23063-4_4","volume-title":"Business Process Management","author":"A Kheldoun","year":"2015","unstructured":"Kheldoun, A., Barkaoui, K., Ioualalen, M.: Specification and verification of complex business processes - a high-level petri net-based approach. In: Motahari-Nezhad, H.R., Recker, J., Weidlich, M. (eds.) BPM 2015. LNCS, vol. 9253, pp. 55\u201371. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23063-4_4"},{"key":"5_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09931-6","volume-title":"A Rigorous Semantics for BPMN 2.0 Process Diagrams","author":"F Kossak","year":"2014","unstructured":"Kossak, F.: A Rigorous Semantics for BPMN 2.0 Process Diagrams. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09931-6"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-31984-9_3","volume-title":"Fundamental Approaches to Software Engineering","author":"A Martens","year":"2005","unstructured":"Martens, A.: Analyzing web service based business processes. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 19\u201333. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31984-9_3"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Mateescu, R., Sala\u00fcn, G., Ye, L.: Quantifying the parallelism in BPMN processes using model checking. In: Proceedings of CBSE, pp. 159\u2013168. ACM (2014)","DOI":"10.1145\/2602458.2602473"},{"issue":"1","key":"5_CR20","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Compu. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theor. Compu. Sci."},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J Meseguer","year":"1998","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Presicce, F.P. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18\u201361. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-64299-4_26"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/978-3-642-34321-6_36","volume-title":"Service-Oriented Computing","author":"HN Nguyen","year":"2012","unstructured":"Nguyen, H.N., Poizat, P., Za\u00efdi, F.: A symbolic framework for the conformance checking of value-passing choreographies. In: Liu, C., Ludwig, H., Toumani, F., Yu, Q. (eds.) ICSOC 2012. LNCS, vol. 7636, pp. 525\u2013532. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34321-6_36"},{"key":"5_CR23","unstructured":"Object Management Group: Business Process Model and Notation (BPMN) - V. 2.0, January 2011"},{"key":"5_CR24","unstructured":"Object Management Group: Decision Model and Notation Specification (DMN) - V. 1.1, May 2016"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Poizat, P., Sala\u00fcn, G.: Checking the realizability of BPMN 2.0 choreographies. In: Proceedings of SAC, pp. 1927\u20131934. ACM (2012)","DOI":"10.1145\/2245276.2232095"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-540-68265-3_16","volume-title":"Coordination Models and Languages","author":"D Prandi","year":"2008","unstructured":"Prandi, D., Quaglia, P., Zannone, N.: Formal analysis of BPMN via a translation into COWS. In: Lea, D., Zavattaro, G. (eds.) COORDINATION 2008. LNCS, vol. 5052, pp. 249\u2013263. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68265-3_16"},{"issue":"1","key":"5_CR27","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.jal.2011.11.002","volume":"10","author":"R Pugliese","year":"2012","unstructured":"Pugliese, R., Tiezzi, F.: A calculus for orchestration of web services. J. Appl. Logic 10(1), 2\u201331 (2012)","journal-title":"J. Appl. Logic"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Raedts, I., Petkovic, M., Usenko, Y.S., van der Werf, J.M., Groote, J.F., Somers, L.: Transformation of BPMN models for behaviour analysis. In: Proceedings of MSVVEIS, pp. 126\u2013137 (2007)","DOI":"10.5220\/0002428801260137"},{"issue":"1","key":"5_CR29","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/j.jlamp.2016.10.001","volume":"86","author":"C Rocha","year":"2017","unstructured":"Rocha, C., Meseguer, J., Mu\u00f1oz, C.: Rewriting modulo SMT and open system analysis. J. Log. Algebr. Methods Program. 86(1), 269\u2013297 (2017)","journal-title":"J. Log. Algebr. Methods Program."},{"issue":"2","key":"5_CR30","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1016\/S0304-3975(01)00366-8","volume":"285","author":"P Viry","year":"2002","unstructured":"Viry, P.: Equational rules for rewriting logic. Theor. Comput. Sci. 285(2), 487\u2013517 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR31","volume-title":"Markov Decision Processes","author":"DJ White","year":"1993","unstructured":"White, D.J.: Markov Decision Processes. Wiley, Chichester (1993)"},{"key":"5_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-88194-0_22","volume-title":"Formal Methods and Software Engineering","author":"PYH Wong","year":"2008","unstructured":"Wong, P.Y.H., Gibbons, J.: A process semantics for BPMN. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 355\u2013374. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88194-0_22"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Wong, P., Gibbons, J.: Verifying business process compatibility. In: Proceedings of QSIC, pp. 126\u2013131. IEEE (2008)","DOI":"10.1109\/QSIC.2008.6"},{"key":"5_CR34","doi-asserted-by":"crossref","unstructured":"Wynn, M.T., Verbeek, H.M.W., van der Aalst, W.M.P., ter Hofstede, A.H.M., Edmond, D.: Business process verification - finally a reality! Bus. Process Manag. J. 15(1), 74\u201392 (2009)","DOI":"10.1108\/14637150910931479"}],"container-title":["Lecture Notes in Computer Science","Rewriting Logic and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99840-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T23:47:53Z","timestamp":1751845673000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99840-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319998398","9783319998404"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99840-4_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}