{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T21:42:37Z","timestamp":1757540557002,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":52,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642230585"},{"type":"electronic","value":"9783642230592"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-23059-2_3","type":"book-chapter","created":{"date-parts":[[2011,8,30]],"date-time":"2011-08-30T13:57:42Z","timestamp":1314712662000},"page":"3-16","source":"Crossref","is-referenced-by-count":13,"title":["Automatic Verification of Data-Centric Business Processes"],"prefix":"10.1007","author":[{"given":"Elio","family":"Damaggio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alin","family":"Deutsch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard","family":"Hull","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Victor","family":"Vianu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Abiteboul, S., Segoufin, L., Vianu, V.: Static analysis of active XML systems. ACM Trans. Database Syst.\u00a034(4) (2009)","DOI":"10.1145\/1620585.1620590"},{"issue":"2","key":"3_CR2","first-page":"236","volume":"61","author":"S. Abiteboul","year":"2000","unstructured":"Abiteboul, S., Vianu, V., Fordham, B.S., Yesha, Y.: Relational transducers for electronic commerce. JCSS\u00a061(2), 236\u2013269 (2000), Extended abstract in PODS 1998","journal-title":"JCSS"},{"key":"3_CR3","series-title":"LNCS","first-page":"379","volume-title":"BPM 2011","author":"B.B. Hariri","year":"2011","unstructured":"Hariri, B.B., Calvanese, D., De Giacomo, G., De Masellis, R., Felli, P.: Foundations of relational artifacts verification. In: Rinderle, S., Toumani, F., Wolf, K. (eds.) BPM 2011. LNCS, vol.\u00a06896, pp. 379\u2013395. Springer, Heidelberg (2011)"},{"issue":"4","key":"3_CR4","doi-asserted-by":"publisher","first-page":"703","DOI":"10.1147\/sj.464.0703","volume":"46","author":"K. Bhattacharya","year":"2007","unstructured":"Bhattacharya, K., Caswell, N.S., Kumaran, S., Nigam, A., Wu, F.Y.: Artifact-centered operational modeling: Lessons from customer engagements. IBM Systems Journal\u00a046(4), 703\u2013721 (2007)","journal-title":"IBM Systems Journal"},{"issue":"1","key":"3_CR5","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1147\/sj.441.0145","volume":"44","author":"K. Bhattacharya","year":"2005","unstructured":"Bhattacharya, K., et al.: A model-driven approach to industrializing discovery processes in pharmaceutical research. IBM Systems Journal\u00a044(1), 145\u2013162 (2005)","journal-title":"IBM Systems Journal"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-540-75183-0_21","volume-title":"Business Process Management","author":"K. Bhattacharya","year":"2007","unstructured":"Bhattacharya, K., Gerede, C.E., Hull, R., Liu, R., Su, J.: Towards formal analysis of artifact-centric business process models. In: Alonso, G., Dadam, P., Rosemann, M. (eds.) BPM 2007. LNCS, vol.\u00a04714, pp. 288\u2013304. Springer, Heidelberg (2007)"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Bojanczyk, M., Muscholl, A., Schwentick, T., Segoufin, L., David, C.: Two-variable logic on words with data. In: LICS, pp. 7\u201316 (2006)","DOI":"10.1109\/LICS.2006.51"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-74240-1_1","volume-title":"Fundamentals of Computation Theory","author":"A. Bouajjani","year":"2007","unstructured":"Bouajjani, A., Habermehl, P., Jurski, Y., Sighireanu, M.: Rewriting systems with data. In: Csuhaj-Varj\u00fa, E., \u00c9sik, Z. (eds.) FCT 2007. LNCS, vol.\u00a04639, pp. 1\u201322. Springer, Heidelberg (2007)"},{"key":"3_CR9","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0304-3975(02)00397-3","volume":"295","author":"A. Bouajjani","year":"2003","unstructured":"Bouajjani, A., Habermehl, P., Mayr, R.: Automatic verification of recursive procedures with one integer parameter. Theoretical Computer Science\u00a0295, 85\u2013106 (2003)","journal-title":"Theoretical Computer Science"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"690","DOI":"10.1007\/978-3-540-71209-1_54","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Bouajjani","year":"2007","unstructured":"Bouajjani, A., Jurski, Y., Sighireanu, M.: A generic framework for reasoning about dynamic networks of infinite-state processes. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 690\u2013705. Springer, Heidelberg (2007)"},{"issue":"2","key":"3_CR11","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/S0020-0190(02)00229-6","volume":"84","author":"P. Bouyer","year":"2002","unstructured":"Bouyer, P.: A logical characterization of data languages. Information Processing Letters\u00a084(2), 75\u201385 (2002)","journal-title":"Information Processing Letters"},{"issue":"2","key":"3_CR12","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/S0890-5401(03)00038-5","volume":"182","author":"P. Bouyer","year":"2003","unstructured":"Bouyer, P., Petit, A., Th\u00e9rien, D.: An algebraic approach to data languages and timed languages. Information and Computation\u00a0182(2), 137\u2013162 (2003)","journal-title":"Information and Computation"},{"key":"3_CR13","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1016\/B978-044482830-9\/50027-8","volume-title":"Handbook of Process Algebra","author":"O. Burkart","year":"2001","unstructured":"Burkart, O., Caucal, D., Moller, F., Steffen, B.: Verification of infinite structures. In: Handbook of Process Algebra, pp. 545\u2013623. Elsevier Science, Amsterdam (2001)"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-642-10383-4_9","volume-title":"Service-Oriented Computing","author":"D. Calvanese","year":"2009","unstructured":"Calvanese, D., De Giacomo, G., Hull, R., Su, J.: Artifact-centric workflow dominance. In: Baresi, L., Chi, C.-H., Suzuki, J. (eds.) ICSOC-ServiceWave 2009. LNCS, vol.\u00a05900, pp. 130\u2013143. Springer, Heidelberg (2009)"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-642-03848-8_18","volume-title":"Business Process Management","author":"T. Chao","year":"2009","unstructured":"Chao, T., et al.: Artifact-based transformation of IBM Global Financing: A case study. In: Dayal, U., Eder, J., Koehler, J., Reijers, H.A. (eds.) BPM 2009. LNCS, vol.\u00a05701, pp. 261\u2013277. Springer, Heidelberg (2009)"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Damaggio, E., Deutsch, A., Vianu, V.: Artifact systems with data dependencies and arithmetic. In: Int\u2019l. Conf. on Database Theory, ICDT (2011)","DOI":"10.1145\/1938551.1938563"},{"key":"3_CR17","series-title":"LNCS","first-page":"385","volume-title":"BPM 2011","author":"E. Damaggio","year":"2011","unstructured":"Damaggio, E., Hull, R., Vaculin, R.: On the equivalence of incremental and fixpoint semantics for business artifacts with guard-stage-milestone lifecycles. In: Rinderle, S., Toumani, F., Wolf, K. (eds.) BPM 2011. LNCS, vol.\u00a06896, pp. 385\u2013401. Springer, Heidelberg (2011)"},{"key":"3_CR18","unstructured":"de Man, H.: Case management: Cordys approach. BP Trends (February 2009), http:\/\/www.bptrends.com"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Demri, S., Lazi\u0107, R.: LTL with the Freeze Quantifier and Register Automata. In: LICS, pp. 17\u201326 (2006)","DOI":"10.1109\/LICS.2006.31"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1007\/978-3-540-78499-9_34","volume-title":"Foundations of Software Science and Computational Structures","author":"S. Demri","year":"2008","unstructured":"Demri, S., Lazi\u0107, R., Sangnier, A.: Model checking freeze LTL over one-counter automata. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol.\u00a04962, pp. 490\u2013504. Springer, Heidelberg (2008)"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Deutsch, A., Hull, R., Patrizi, F., Vianu, V.: Automatic verification of data-centric business processes. In: ICDT, pp. 252\u2013267 (2009)","DOI":"10.1145\/1514894.1514924"},{"issue":"3","key":"3_CR22","first-page":"442","volume":"73","author":"A. Deutsch","year":"2007","unstructured":"Deutsch, A., Sui, L., Vianu, V.: Specification and verification of data-driven web applications. JCSS\u00a073(3), 442\u2013474 (2007)","journal-title":"JCSS"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Deutsch, A., Sui, L., Vianu, V., Zhou, D.: A system for specification and verification of interactive, data-driven web applications. In: SIGMOD Conference (2006)","DOI":"10.1145\/1142473.1142584"},{"key":"3_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/3-540-44543-9_10","volume-title":"Research Issues in Structured and Semistructured Database Programming","author":"G. Dong","year":"2000","unstructured":"Dong, G., Hull, R., Kumar, B., Su, J., Zhou, G.: A framework for optimizing distributed workflow executions. In: Connor, R.C.H., Mendelzon, A.O. (eds.) DBPL 1999. LNCS, vol.\u00a01949, pp. 152\u2013167. Springer, Heidelberg (2000)"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Hull, R., et al.: Introducing the guard-stage-milestone approach for specifying business entity lifecycles. In: Proc. of 7th Intl. Workshop on Web Services and Formal Methods, WS-FM, pp. 1\u201324 (2010)","DOI":"10.1007\/978-3-642-19589-1_1"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Gerede, C.E., Bhattacharya, K., Su, J.: Static analysis of business artifact-centric operational models. In: IEEE International Conference on Service-Oriented Computing and Applications (2007)","DOI":"10.1109\/SOCA.2007.42"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-540-74974-5_15","volume-title":"Service-Oriented Computing \u2013 ICSOC 2007","author":"C.E. Gerede","year":"2007","unstructured":"Gerede, C.E., Su, J.: Specification and verification of artifact behaviors in business process models. In: Kr\u00e4mer, B.J., Lin, K.-J., Narasimhan, P. (eds.) ICSOC 2007. LNCS, vol.\u00a04749, pp. 181\u2013192. Springer, Heidelberg (2007), http:\/\/www.springerlink.com\/content\/c371144007878627"},{"key":"3_CR28","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2475.001.0001","volume-title":"Document Engineering: Analyzing and Designing Documents for Business Informatics and Web Services","author":"R.J. Glushko","year":"2005","unstructured":"Glushko, R.J., McGrath, T.: Document Engineering: Analyzing and Designing Documents for Business Informatics and Web Services. MIT Press, Cmabridge (2005)"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Hull, R., Damaggio, E., De Masellis, R., Fournier, F., Gupta, M., Heath III, F., Hobson, S., Linehan, M., Maradugu, S., Nigam, A., Sukaviriya, P., Vacul\u00edn, R.: Business artifacts with guard-stage-milestone lifecycles: Managing artifact interactions with conditions and events. In: ACM Intl. Conf. on Distributed Event-based Systems, DEBS (2011)","DOI":"10.1145\/2002259.2002270"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Hull, R., Llirbat, F., Kumar, B., Zhou, G., Dong, G., Su, J.: Optimization techniques for data-intensive decision flows. In: Proc. IEEE Intl. Conf. on Data Engineering (ICDE), pp. 281\u2013292 (2000)","DOI":"10.1109\/ICDE.2000.839420"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Hull, R., Llirbat, F., Simon, E., Su, J., Dong, G., Kumar, B., Zhou, G.: Declarative workflows that support easy modification and dynamic browsing. In: Proc. Int. Joint Conf. on Work Activities Coordination and Collaboration (1999)","DOI":"10.1145\/295665.295674"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Jurdzinski, M., Lazi\u0107, R.: Alternation-free modal mu-calculus for data trees. In: LICS, pp. 131\u2013140 (2007)","DOI":"10.1109\/LICS.2007.11"},{"key":"3_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-540-69534-9_3","volume-title":"Advanced Information Systems Engineering","author":"S. Kumaran","year":"2008","unstructured":"Kumaran, S., Liu, R., Wu, F.Y.: On the duality of information-centric and activity-centric models of business processes. In: Bellahs\u00e8ne, Z., L\u00e9onard, M. (eds.) CAiSE 2008. LNCS, vol.\u00a05074, pp. 32\u201347. Springer, Heidelberg (2008)"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"Kumaran, S., Nandi, P., Heath, T., Bhaskaran, K., Das, R.: ADoc-oriented programming. In: Symp. on Applications and the Internet (SAINT), pp. 334\u2013343 (2003)","DOI":"10.1109\/SAINT.2003.1183067"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-540-75183-0_13","volume-title":"Business Process Management","author":"J. K\u00fcster","year":"2007","unstructured":"K\u00fcster, J., Ryndina, K., Gall, H.: Generation of BPM for object life cycle compliance. In: Alonso, G., Dadam, P., Rosemann, M. (eds.) BPM 2007. LNCS, vol.\u00a04714, pp. 165\u2013181. Springer, Heidelberg (2007)"},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-540-73094-1_19","volume-title":"Petri Nets and Other Models of Concurrency \u2013 ICATPN 2007","author":"R. Lazi\u0107","year":"2007","unstructured":"Lazi\u0107, R., Newcomb, T., Ouaknine, J., Roscoe, A., Worrell, J.: Nets with tokens which carry data. In: Kleijn, J., Yakovlev, A. (eds.) ICATPN 2007. LNCS, vol.\u00a04546, pp. 301\u2013320. Springer, Heidelberg (2007)"},{"key":"3_CR37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07003-1","volume-title":"Elements of Finite Model Theory","author":"L. Libkin","year":"2004","unstructured":"Libkin, L.: Elements of Finite Model Theory. Springer, Heidelberg (2004)"},{"key":"3_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-540-72988-4_23","volume-title":"Advanced Information Systems Engineering","author":"R. Liu","year":"2007","unstructured":"Liu, R., Bhattacharya, K., Wu, F.Y.: Modeling business contexture and behavior using business artifacts. In: Krogstie, J., Opdahl, A.L., Sindre, G. (eds.) CAiSE 2007 and WES 2007. LNCS, vol.\u00a04495, pp. 324\u2013339. Springer, Heidelberg (2007)"},{"key":"3_CR39","unstructured":"Martin, D., et al.: OWL-S: Semantic markup for web services, W3C Member Submission (November 2003)"},{"issue":"2","key":"3_CR40","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1109\/5254.920599","volume":"16","author":"S.A. McIlraith","year":"2001","unstructured":"McIlraith, S.A., Son, T.C., Zeng, H.: Semantic web services. IEEE Intelligent Systems\u00a016(2), 46\u201353 (2001)","journal-title":"IEEE Intelligent Systems"},{"key":"3_CR41","volume-title":"Computation: finite and infinite machines","author":"M.L. Minsky","year":"1967","unstructured":"Minsky, M.L.: Computation: finite and infinite machines. Prentice-Hall, Inc., Upper Saddle River (1967)"},{"key":"3_CR42","unstructured":"Nandi, P., et al.: Data4BPM, Part 1: Introducing Business Entities and the Business Entity Definition Language (BEDL) (April 2010), http:\/\/www.ibm.com\/developerworks\/websphere\/library\/techarticles\/1004_nandi\/1004_nandi.html"},{"key":"3_CR43","doi-asserted-by":"crossref","unstructured":"Nandi, P., Kumaran, S.: Adaptive business objects \u2013 a new component model for business integration. In: Proc. Intl. Conf. on Enterprise Information Systems, pp. 179\u2013188 (2005)","DOI":"10.5220\/0002553301790188"},{"key":"3_CR44","doi-asserted-by":"crossref","unstructured":"Narayanan, S., McIlraith, S.: Simulation, verification and automated composition of web services. In: Intl. World Wide Web Conf, (WWW 2002) (2002)","DOI":"10.1145\/511446.511457"},{"issue":"3","key":"3_CR45","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/1013560.1013562","volume":"5","author":"F. Neven","year":"2004","unstructured":"Neven, F., Schwentick, T., Vianu, V.: Finite State Machines for Strings Over Infinite Alphabets. ACM Transactions on Computational Logic\u00a05(3), 403\u2013435 (2004)","journal-title":"ACM Transactions on Computational Logic"},{"issue":"3","key":"3_CR46","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1147\/sj.423.0428","volume":"42","author":"A. Nigam","year":"2003","unstructured":"Nigam, A., Caswell, N.S.: Business artifacts: An approach to operational specification. IBM Systems Journal\u00a042(3), 428\u2013445 (2003)","journal-title":"IBM Systems Journal"},{"key":"3_CR47","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":"3_CR48","unstructured":"Segoufin, L., Torunczyk, S.: Automata based verification over linearly ordered data domains. In: Int\u2019l. Symp. on Theoretical Aspects of Computer Science, STACS (2011)"},{"issue":"1","key":"3_CR49","first-page":"40","volume":"66","author":"M. Spielmann","year":"2003","unstructured":"Spielmann, M.: Verification of relational transducers for electronic commerce. JCSS\u00a066(1), 40\u201365 (2003), Extended abstract in PODS 2000","journal-title":"JCSS"},{"key":"3_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/11538394_19","volume-title":"Business Process Management","author":"J. Wang","year":"2005","unstructured":"Wang, J., Kumar, A.: A framework for document-driven workflow systems. In: van der Aalst, W.M.P., Benatallah, B., Casati, F., Curbera, F. (eds.) BPM 2005. LNCS, vol.\u00a03649, pp. 285\u2013301. Springer, Heidelberg (2005)"},{"key":"3_CR51","doi-asserted-by":"crossref","unstructured":"Zhao, X., Su, J., Yang, H., Qiu, Z.: Enforcing constraints on life cycles of business artifacts. In: TASE, pp. 111\u2013118 (2009)","DOI":"10.1109\/TASE.2009.46"},{"key":"3_CR52","unstructured":"Zhu, W.-D., et al.: Advanced Case Management with IBM Case Manager. Published by IBM, http:\/\/www.redbooks.ibm.com\/redpieces\/abstracts\/sg247929.html?Open"}],"container-title":["Lecture Notes in Computer Science","Business Process Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-23059-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,9]],"date-time":"2025-03-09T12:14:35Z","timestamp":1741522475000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-23059-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642230585","9783642230592"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-23059-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}