{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T05:57:21Z","timestamp":1777528641445,"version":"3.51.4"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2012,8,1]],"date-time":"2012-08-01T00:00:00Z","timestamp":1343779200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000145","name":"Division of Information and Intelligent Systems","doi-asserted-by":"publisher","award":["IIS-0916515"],"award-info":[{"award-number":["IIS-0916515"]}],"id":[{"id":"10.13039\/100000145","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Database Syst."],"published-print":{"date-parts":[[2012,8]]},"abstract":"<jats:p>\n            We study the static verification problem for data-centric business processes, specified in a variant of IBM's \u201cbusiness artifact\u201d model. Artifacts are records of variables that correspond to business-relevant objects and are updated by a set of services equipped with pre- and postconditions, that implement business process tasks. The verification problem consists in statically checking whether all runs of an artifact system satisfy desirable properties expressed in a first-order extension of linear-time temporal logic. Previous work identified the class of\n            <jats:italic>guarded<\/jats:italic>\n            artifact systems and properties, for which verification is decidable. However, the results suffer an important limitation: they fail in the presence of even very simple data dependencies or arithmetic, both crucial to real-life business processes. In this article, we extend the artifact model and verification results to alleviate this limitation. We identify a practically significant class of business artifacts with data dependencies and arithmetic, for which verification is decidable. The technical machinery needed to establish the results is fundamentally different from previous work. While the worst-case complexity of verification is nonelementary, we identify various realistic restrictions yielding more palatable upper bounds.\n          <\/jats:p>","DOI":"10.1145\/2338626.2338628","type":"journal-article","created":{"date-parts":[[2012,9,11]],"date-time":"2012-09-11T22:21:06Z","timestamp":1347402066000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":44,"title":["Artifact systems with data dependencies and arithmetic"],"prefix":"10.1145","volume":"37","author":[{"given":"Elio","family":"Damaggio","sequence":"first","affiliation":[{"name":"Microsoft"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alin","family":"Deutsch","sequence":"additional","affiliation":[{"name":"University of California, San Diego, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Victor","family":"Vianu","sequence":"additional","affiliation":[{"name":"University of California, San Diego, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,9,6]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/237661.237674"},{"key":"e_1_2_2_2_1","unstructured":"Abiteboul S. Hull R. and Vianu V. 1995. Foundations of Databases. Addison Wesley.   Abiteboul S. Hull R. and Vianu V. 1995. Foundations of Databases. Addison Wesley."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1620585.1620590"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2000.1708"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1147\/sj.441.0145"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1147\/sj.464.0703"},{"key":"e_1_2_2_7_1","volume-title":"Proceedings of the International Conference on Business Process Management (BPM'07)","author":"Bhattacharya K.","unstructured":"Bhattacharya , K. , Gerede , C. E. , Hull , R. , Liu , R. , and Su , J . 2007b. Towards formal analysis of artifact-centric business process models . In Proceedings of the International Conference on Business Process Management (BPM'07) . 288--304. Bhattacharya, K., Gerede, C. E., Hull, R., Liu, R., and Su, J. 2007b. Towards formal analysis of artifact-centric business process models. In Proceedings of the International Conference on Business Process Management (BPM'07). 288--304."},{"key":"e_1_2_2_8_1","first-page":"191","article-title":"Two-Way automata and length-preserving homomorphisms","volume":"29","author":"Birget J.-C.","year":"1996","unstructured":"Birget , J.-C. 1996 . Two-Way automata and length-preserving homomorphisms . Theory Comput. Syst. 29 , 3, 191 -- 226 . Birget, J.-C. 1996. Two-Way automata and length-preserving homomorphisms. Theory Comput. Syst. 29, 3, 191--226.","journal-title":"Theory Comput. Syst."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.51"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74240-1_1"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763507.1763578"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00397-3"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(02)00229-6"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00038-5"},{"key":"e_1_2_2_15_1","doi-asserted-by":"crossref","unstructured":"Burkart O. Caucal D. Moller F. and Steffen B. 2001. Verification of infinite structures. In Handbook of Process Algebra Elsevier Science 545--623.  Burkart O. Caucal D. Moller F. and Steffen B. 2001. Verification of infinite structures. In Handbook of Process Algebra Elsevier Science 545--623.","DOI":"10.1016\/B978-044482830-9\/50027-8"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10383-4_9"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1938551.1938563"},{"key":"e_1_2_2_19_1","volume-title":"Proceedings of the International Conference on Business Process Management (BPM'11)","author":"Damaggio E.","unstructured":"Damaggio , E. , Hull , R. , and Vaculin , R . 2011b. On the equivalence of incremental and fixpoint semantics for business entities with guard-stage-milestone lifecycles . In Proceedings of the International Conference on Business Process Management (BPM'11) . Damaggio, E., Hull, R., and Vaculin, R. 2011b. On the equivalence of incremental and fixpoint semantics for business entities with guard-stage-milestone lifecycles. In Proceedings of the International Conference on Business Process Management (BPM'11)."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.31"},{"key":"e_1_2_2_21_1","volume-title":"Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08)","author":"Demri S.","unstructured":"Demri , S. , Lazi\u0107 , R. , and Sangnier , A . 2008. Model checking freeze LTL over one-counter automata . In Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08) . 490--504. Demri, S., Lazi\u0107, R., and Sangnier, A. 2008. Model checking freeze LTL over one-counter automata. In Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'08). 490--504."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.02.021"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1376916.1376938"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1514894.1514924"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2006.10.006"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1142351.1142364"},{"key":"e_1_2_2_27_1","volume-title":"Proceedings of the International Workshop on Database Programming Languages (DBPL'99)","author":"Dong G.","unstructured":"Dong , G. , Hull , R. , Kumar , B. , Su , J. , and Zhou , G . 1999. A framework for optimizing distributed workflow executions . In Proceedings of the International Workshop on Database Programming Languages (DBPL'99) . 152--167. Dong, G., Hull, R., Kumar, B., Su, J., and Zhou, G. 1999. A framework for optimizing distributed workflow executions. In Proceedings of the International Workshop on Database Programming Languages (DBPL'99). 152--167."},{"key":"e_1_2_2_28_1","volume-title":"Handbook of Theoretical Computer Science","author":"Emerson E. A.","unstructured":"Emerson , E. A. 1990. Temporal and modal logic . In Handbook of Theoretical Computer Science , vol. B: Formal Models and Semantics, J. V . Leeuwen, Ed ., North-Holland\/MIT Press , 995--1072. Emerson, E. A. 1990. Temporal and modal logic. In Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, J. V. Leeuwen, Ed., North-Holland\/MIT Press, 995--1072."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/322344.322347"},{"key":"e_1_2_2_30_1","volume-title":"Proceedings of the International Conference on Database Theory (ICDT'03)","author":"Fagin R.","unstructured":"Fagin , R. , Kolaitis , P. G. , Miller , R. J. , and Popa , L . 2003. Data exchange: Semantics and query answering . In Proceedings of the International Conference on Database Theory (ICDT'03) . 207--224. Fagin, R., Kolaitis, P. G., Miller, R. J., and Popa, L. 2003. Data exchange: Semantics and query answering. In Proceedings of the International Conference on Database Theory (ICDT'03). 207--224."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1514894.1514922"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/SOCA.2007.42"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74974-5_15"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/1796125"},{"key":"e_1_2_2_35_1","volume-title":"Proceedings of the International Workshop on Web Services and Formal Methods (WS-FM'10)","author":"Hull R.","unstructured":"Hull , R. , Damaggio , E. , Fournier , F. , Gupta , M. , Heath , F. T. , Hobson , S. , Linehan , M. H. , Maradugu , S. , Nigam , A. , Sukaviriya , P. , and Vaculin , R . 2010. Introducing the guard-stage-milestone approach for specifying business entity lifecycles . In Proceedings of the International Workshop on Web Services and Formal Methods (WS-FM'10) . 1--24. Hull, R., Damaggio, E., Fournier, F., Gupta, M., Heath, F. T., Hobson, S., Linehan, M. H., Maradugu, S., Nigam, A., Sukaviriya, P., and Vaculin, R. 2010. Introducing the guard-stage-milestone approach for specifying business entity lifecycles. In Proceedings of the International Workshop on Web Services and Formal Methods (WS-FM'10). 1--24."},{"key":"e_1_2_2_36_1","volume-title":"Proceedings of the IEEE International Conference on Data Engineering (ICDE'00)","author":"Hull R.","unstructured":"Hull , R. , Llirbat , F. , Kumar , B. , Zhou , G. , Dong , G. , and Su , J . 2000. Optimization techniques for data-intensive decision flows . In Proceedings of the IEEE International Conference on Data Engineering (ICDE'00) . 281--292. Hull, R., Llirbat, F., Kumar, B., Zhou, G., Dong, G., and Su, J. 2000. Optimization techniques for data-intensive decision flows. In Proceedings of the IEEE International Conference on Data Engineering (ICDE'00). 281--292."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/295665.295674"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/322047.322058"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.11"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/800057.808695"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69534-9_3"},{"key":"e_1_2_2_42_1","volume-title":"Proceedings of the Symposium on Applications and the Internet (SAINT'03)","author":"Kumaran S.","unstructured":"Kumaran , S. , Nandi , P. , Heath , T. , Bhaskaran , K. , and Das , R . 2003. ADoc-Oriented programming . In Proceedings of the Symposium on Applications and the Internet (SAINT'03) . 334--343. Kumaran, S., Nandi, P., Heath, T., Bhaskaran, K., and Das, R. 2003. ADoc-Oriented programming. In Proceedings of the Symposium on Applications and the Internet (SAINT'03). 334--343."},{"key":"e_1_2_2_43_1","volume-title":"Proceedings of the 5th International Conference on Business Process Management (BPM'07)","author":"K\u00fcster J.","unstructured":"K\u00fcster , J. , Ryndina , K. , and Gall , H . 2007. Generation of bpm for object life cycle compliance . In Proceedings of the 5th International Conference on Business Process Management (BPM'07) . K\u00fcster, J., Ryndina, K., and Gall, H. 2007. Generation of bpm for object life cycle compliance. In Proceedings of the 5th International Conference on Business Process Management (BPM'07)."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1137\/0213010"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/1769053.1769074"},{"key":"e_1_2_2_46_1","volume-title":"Elements of Finite Model Theory","author":"Libkin L.","unstructured":"Libkin , L. 2004. Elements of Finite Model Theory . Springer . Libkin, L. 2004. Elements of Finite Model Theory. Springer."},{"key":"e_1_2_2_47_1","volume-title":"Proceedings of the International Conference on Advanced Information Systems Engineering (CAISE'07)","volume":"4495","author":"Liu R.","unstructured":"Liu , R. , Bhattacharya , K. , and Wu , F. Y . 2007. Modeling business contexture and behavior using business artifacts . In Proceedings of the International Conference on Advanced Information Systems Engineering (CAISE'07) . Lecture Notes in Computer Science , vol. 4495 , Springer. Liu, R., Bhattacharya, K., and Wu, F. Y. 2007. Modeling business contexture and behavior using business artifacts. In Proceedings of the International Conference on Advanced Information Systems Engineering (CAISE'07). Lecture Notes in Computer Science, vol. 4495, Springer."},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.01.002"},{"key":"e_1_2_2_49_1","unstructured":"Martin D. Burstein M. Hobbs J. Lassila O. McDermott D. McIlraith S. Narayanan S. Paolucci M. Parsia B. Payne T. Sirin E. Srinivasan N. and Sycara K. 2003. OWL-S: Semantic markup for Web services. W3C member submission.  Martin D. Burstein M. Hobbs J. Lassila O. McDermott D. McIlraith S. Narayanan S. Paolucci M. Parsia B. Payne T. Sirin E. Srinivasan N. and Sycara K. 2003. OWL-S: Semantic markup for Web services. W3C member submission."},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/5254.920599"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1807085.1807102"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.5555\/1095587"},{"key":"e_1_2_2_53_1","volume-title":"Proceedings of the International Conference on Enterprise Information Systems. 179--188","author":"Nandi P.","unstructured":"Nandi , P. and Kumaran , S . 2005. Adaptive business objects -- A new component model for business integration . In Proceedings of the International Conference on Enterprise Information Systems. 179--188 . Nandi, P. and Kumaran, S. 2005. Adaptive business objects -- A new component model for business integration. In Proceedings of the International Conference on Enterprise Information Systems. 179--188."},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/511446.511457"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1013560.1013562"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1147\/sj.423.0428"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/11431855_16"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/11568322_23"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/11767138_20"},{"key":"e_1_2_2_61_1","volume-title":"International Symposium on Theoretical Aspects of Computer Science (STACS'11)","author":"Segoufin L.","unstructured":"Segoufin , L. and Torunczyk , S . 2011. Automata based verification over linearly ordered data domains . In International Symposium on Theoretical Aspects of Computer Science (STACS'11) . Segoufin, L. and Torunczyk, S. 2011. Automata based verification over linearly ordered data domains. In International Symposium on Theoretical Aspects of Computer Science (STACS'11)."},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(02)00029-6"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/11538394_19"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2009.46"}],"container-title":["ACM Transactions on Database Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2338626.2338628","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2338626.2338628","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:49:00Z","timestamp":1750236540000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2338626.2338628"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,8]]},"references-count":63,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["10.1145\/2338626.2338628"],"URL":"https:\/\/doi.org\/10.1145\/2338626.2338628","relation":{},"ISSN":["0362-5915","1557-4644"],"issn-type":[{"value":"0362-5915","type":"print"},{"value":"1557-4644","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,8]]},"assertion":[{"value":"2011-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-09-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}