{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T14:40:03Z","timestamp":1748702403646,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662486153"},{"type":"electronic","value":"9783662486160"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","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":[[2015]]},"DOI":"10.1007\/978-3-662-48616-0_16","type":"book-chapter","created":{"date-parts":[[2015,11,24]],"date-time":"2015-11-24T16:18:43Z","timestamp":1448381923000},"page":"253-268","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Verification of GSM-Based Artifact-Centric Systems by Predicate Abstraction"],"prefix":"10.1007","author":[{"given":"Pavel","family":"Gonzalez","sequence":"first","affiliation":[]},{"given":"Andreas","family":"Griesmayer","sequence":"additional","affiliation":[]},{"given":"Alessio","family":"Lomuscio","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,25]]},"reference":[{"issue":"3","key":"16_CR1","first-page":"3","volume":"32","author":"D Cohn","year":"2009","unstructured":"Cohn, D., Hull, R.: Business artifacts: a data-centric approach to modeling business operations and processes. Bull. IEEE Comput. Soc. Tech. Committee Data Eng. 32(3), 3\u20139 (2009)","journal-title":"Bull. IEEE Comput. Soc. Tech. Committee Data Eng."},{"key":"16_CR2","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-36285-9_4","volume-title":"Business Process Management Workshops","author":"M Marin","year":"2013","unstructured":"Marin, M., Hull, R., Vacul\u00edn, R.: Data centric BPM and the emerging case management standard: a short survey. In: La Rosa, M., Soffer, P. (eds.) BPM Workshops 2012. LNBIP, vol. 132, pp. 24\u201330. Springer, Heidelberg (2013)"},{"key":"16_CR3","unstructured":"Heath, F.T., Hull, R., Vaculin, R.: Barcelona: a design and runtime environment for modeling and execution of artifact-centric business processes. In: Demo Track in International Conference on Business Process Management 2011 (2011)"},{"key":"16_CR4","unstructured":"Boaz, D., Heath, T., Gupta, M., Limonad, L., Sun, Y., Hull, R., Vacul\u00edn, R.: The ACSI hub: a data-centric environment for service interoperation. In: Proceedings of the BPM Demo Sessions 2014 Co-located with the 12th International Conference on Business Process Management (BPM 2014). Volume 1295 of CEUR Workshop Proceedings, CEUR-WS.org (2014)"},{"issue":"6","key":"16_CR5","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1049\/iet-sen:20070027","volume":"1","author":"L Baresi","year":"2007","unstructured":"Baresi, L., Bianculli, D., Ghezzi, C., Guinea, S., Spoletini, P.: Validation of web service compositions. IET Softw. 1(6), 219\u2013232 (2007)","journal-title":"IET Softw."},{"key":"16_CR6","series-title":"Data-Centric Systems and Applications","volume-title":"Web Services - Concepts Architectures and Applications","author":"G Alonso","year":"2004","unstructured":"Alonso, G., Casati, F., Kuno, H.A., Machiraju, V.: Web Services - Concepts Architectures and Applications. Data-Centric Systems and Applications. Springer, Heidelberg (2004)"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-25535-9_10","volume-title":"Service-Oriented Computing","author":"F Belardinelli","year":"2011","unstructured":"Belardinelli, F., Lomuscio, A., Patrizi, F.: Verification of deployed artifact systems via data abstraction. In: Kappel, G., Maamar, Z., Motahari-Nezhad, H.R. (eds.) Service Oriented Computing. LNCS, vol. 7084, pp. 142\u2013156. Springer, Heidelberg (2011)"},{"key":"16_CR9","unstructured":"Belardinelli, F., Lomuscio, A., Patrizi, F.: An abstraction technique for the verification of artifact-centric systems. In: Proceedings of Principles of Knowledge Representation and Reasoning (KR 2012), pp. 319\u2013328 (2012)"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-34321-6_2","volume-title":"Service-Oriented Computing","author":"F Belardinelli","year":"2012","unstructured":"Belardinelli, F., Lomuscio, A., Patrizi, F.: Verification of GSM-based artifact-centric systems through finite abstraction. In: Liu, C., Ludwig, H., Toumani, F., Yu, Q. (eds.) Service Oriented Computing. LNCS, vol. 7636, pp. 17\u201331. Springer, Heidelberg (2012)"},{"key":"16_CR11","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. 4714, pp. 288\u2013304. Springer, Heidelberg (2007)"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Deutsch, A., Hull, R., Patrizi, F., Vianu, V.: Automatic verification of data-centric business processes. In: Proceedings of the 12th International Conference on Database Theory (ICDT 2009), Volume 361 of ACM International Conference Proceeding Series, pp. 252\u2013267. ACM (2009)","DOI":"10.1145\/1514894.1514924"},{"key":"16_CR13","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1613\/jair.4424","volume":"51","author":"F Belardinelli","year":"2014","unstructured":"Belardinelli, F., Lomuscio, A., Patrizi, F.: Verification of agent-based artifact systems. J. Artif. Intel. Res. 51, 333\u2013376 (2014)","journal-title":"J. Artif. Intel. Res."},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Gonzalez, P., Griesmayer, A., Lomuscio, A.: Verifying GSM-based business artifacts. In: Proceedings of the IEEE International Conference on Web Services (ICWS 2012), pp. 25\u201332 (2012)","DOI":"10.1109\/ICWS.2012.31"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-319-06859-6_6","volume-title":"Service-Oriented Computing \u2013 ICSOC 2013 Workshops","author":"P Gonzalez","year":"2014","unstructured":"Gonzalez, P., Griesmayer, A., Lomuscio, A.: Model checking GSM-based multi-agent systems. In: Lomuscio, A.R., Nepal, S., Patrizi, F., Benatallah, B., Brandi\u0107, I. (eds.) ICSOC 2013. LNCS, vol. 8377, pp. 54\u201368. Springer, Heidelberg (2014)"},{"issue":"11","key":"16_CR16","doi-asserted-by":"publisher","first-page":"1313","DOI":"10.1016\/j.ic.2008.07.004","volume":"206","author":"S Shoham","year":"2008","unstructured":"Shoham, S., Grumberg, O.: 3-valued abstraction: more precision at less cost. Inf. Computat. 206(11), 1313\u20131333 (2008)","journal-title":"Inf. Computat."},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Hull, R., et al.: Business artifacts with guard-stage-milestone lifecycles: managing artifact interactions with conditions and events. In: Proceedings of the 5th ACM International Conference on Distributed Event-Based Systems (DEBS 2011) (2011)","DOI":"10.1145\/2002259.2002270"},{"key":"16_CR18","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning about Knowledge","author":"R Fagin","year":"1995","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. The MIT Press, Cambridge (1995)"},{"issue":"4","key":"16_CR19","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1145\/990010.990011","volume":"12","author":"M Chechik","year":"2003","unstructured":"Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-valued symbolic model-checking. ACM Trans. Softw. Eng. Methodol. 12(4), 371\u2013408 (2003)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"16_CR20","unstructured":"Bozianu, R., Dima, C., Enea, C.: Model-checking an epistemic $$\\mu $$-calculus with synchronous and perfect recall semantics (2013). CoRR abs\/1310.6434"},{"issue":"3","key":"16_CR21","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$-calculus. Theor. Comput. Sci. 27(3), 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR22","unstructured":"Gonzalez, P., Griesmayer, A., Lomuscio, A.: GSMC: a model checker for GSM (2014). http:\/\/vas.doc.ic.ac.uk\/software\/extensions\/"},{"key":"16_CR23","unstructured":"Somenzi, F.: CUDD: CU decision diagram package release 2.5.0 (2012). http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/"},{"key":"16_CR24","unstructured":"Barrett, C., Tinelli, C.: CVC4 version 1.2 (2013). http:\/\/cvc4.cs.nyu.edu\/web\/"},{"key":"16_CR25","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science: Modelling and Reasoning about Systems","author":"M Huth","year":"2004","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, Cambridge (2004)"},{"key":"16_CR26","unstructured":"Toribio Gomez, D., Murphy-O\u2019Connor, C., De Leenheer, P., Malarme, P.: D5.5 deployment and evaluation of pilots using final ACSI hub system results and evaluation. Project deliverable, The ACSI Project (EU FP7-ICT-257593) (2013)"},{"key":"16_CR27","unstructured":"Group, O.M.: Case management model and notation, version 1.0. Technical report (2014)"}],"container-title":["Lecture Notes in Computer Science","Service-Oriented Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48616-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T14:07:08Z","timestamp":1748700428000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-48616-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662486153","9783662486160"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48616-0_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 November 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}