{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T15:12:46Z","timestamp":1772205166662,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642173578","type":"print"},{"value":"9783642173585","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-45005-1_5","type":"book-chapter","created":{"date-parts":[[2013,11,27]],"date-time":"2013-11-27T09:53:14Z","timestamp":1385545994000},"page":"54-68","source":"Crossref","is-referenced-by-count":6,"title":["Runtime Enforcement of First-Order LTL Properties on Data-Aware Business Processes"],"prefix":"10.1007","author":[{"given":"Riccardo","family":"De Masellis","sequence":"first","affiliation":[]},{"given":"Jianwen","family":"Su","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"Baier, C., Katoen, J.P.: Principles of model checking. MIT Press (2008)"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-14295-6_1","volume-title":"Computer Aided Verification","author":"D. Basin","year":"2010","unstructured":"Basin, D., Klaedtke, F., M\u00fcller, S.: Policy monitoring in first-order temporal logic. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 1\u201318. Springer, Heidelberg (2010)"},{"issue":"4","key":"5_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A. Bauer","year":"2011","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for ltl and tltl. ACM Trans. Softw. Eng. Methodol.\u00a020(4), 14:1\u201314:64 (2011)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"5_CR4","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.) ICSOC 2011. LNCS, vol.\u00a07084, pp. 142\u2013156. Springer, Heidelberg (2011)"},{"key":"5_CR5","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., 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), http:\/\/www.springerlink.com\/content\/w31j312311x6310j"},{"issue":"2","key":"5_CR6","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1145\/210197.210200","volume":"20","author":"J. Chomicki","year":"1995","unstructured":"Chomicki, J.: Efficient checking of temporal integrity constraints using bounded history encoding. ACM Transactions on Database Systems\u00a020(2), 149\u2013186 (1995)","journal-title":"ACM Transactions on Database Systems"},{"key":"5_CR7","volume-title":"Model checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. The MIT Press, Cambridge (1999)"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-23059-2_3","volume-title":"Business Process Management","author":"E. Damaggio","year":"2011","unstructured":"Damaggio, E., Deutsch, A., Hull, R., Vianu, V.: Automatic verification of data-centric business processes. In: Rinderle-Ma, S., Toumani, F., Wolf, K. (eds.) BPM 2011. LNCS, vol.\u00a06896, pp. 3\u201316. Springer, Heidelberg (2011)"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11513988_36","volume-title":"Computer Aided Verification","author":"M. D\u2019Amorim","year":"2005","unstructured":"D\u2019Amorim, M., Ro\u015fu, G.: Efficient monitoring of \u03c9-languages. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 364\u2013378. Springer, Heidelberg (2005)"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"D\u2019Angelo, B., Sankaranarayanan, S., S\u00e1nchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: Lola: Runtime monitoring of synchronous systems. In: TIME, pp. 166\u2013174 (2005)","DOI":"10.1109\/TIME.2005.26"},{"issue":"2","key":"5_CR11","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1142\/S0218843012500025","volume":"21","author":"G. De Giacomo","year":"2012","unstructured":"De Giacomo, G., De Masellis, R., Rosati, R.: Verification of conjunctive artifact-centric services. Int. J. Cooperative Inf. Syst.\u00a021(2), 111\u2013140 (2012)","journal-title":"Int. J. Cooperative Inf. Syst."},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BF01530820","volume":"14","author":"G. Dong","year":"1995","unstructured":"Dong, G., Su, J., Topor, R.: Nonrecursive incremental evaluation of datalog queries. Annals of Mathematics and Artificial Intelligence\u00a014, 187\u2013223 (1995)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-45069-6_3","volume-title":"Computer Aided Verification","author":"C. Eisner","year":"2003","unstructured":"Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 27\u201339. Springer, Heidelberg (2003)"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-642-03848-8_19","volume-title":"Business Process Management","author":"D. Fahland","year":"2009","unstructured":"Fahland, D., Favre, C., Jobstmann, B., Koehler, J., Lohmann, N., V\u00f6lzer, H., Wolf, K.: Instantaneous soundness checking of industrial business process models. In: Dayal, U., Eder, J., Koehler, J., Reijers, H.A. (eds.) BPM 2009. LNCS, vol.\u00a05701, pp. 278\u2013293. Springer, Heidelberg (2009)"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Fitting, M., Mendelsohn, R.L.: First-Order Modal Logic. Kluwer Academic Press (1998)","DOI":"10.1007\/978-94-011-5292-1"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"5_CR17","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":"5_CR18","doi-asserted-by":"crossref","unstructured":"Hall\u00e9, S., Villemaire, R.: Runtime monitoring of message-based workflows with data. In: EDOC, pp. 63\u201372 (2008)","DOI":"10.1109\/EDOC.2008.32"},{"key":"5_CR19","unstructured":"Hariri, B.B., Calvanese, D., De Giacomo, G., De Masellis, R., Felli, P., Montali, M.: Verification of description logic knowledge and action bases. In: ECAI, pp. 103\u2013108 (2012)"},{"issue":"2","key":"5_CR20","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1023\/B:FORM.0000017842.17301.bc","volume":"24","author":"K. Havelund","year":"2004","unstructured":"Havelund, K., Rosu, G.: Foreword - selected papers from the first international workshop on runtime verification held in paris, july 2001 (rv\u201901). Formal Methods in System Design\u00a024(2), 99\u2013100 (2004)","journal-title":"Formal Methods in System Design"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-642-03848-8_20","volume-title":"Business Process Management","author":"K. Klai","year":"2009","unstructured":"Klai, K., Tata, S., Desel, J.: Symbolic abstraction and deadlock-freeness verification of inter-enterprise processes. In: Dayal, U., Eder, J., Koehler, J., Reijers, H.A. (eds.) BPM 2009. LNCS, vol.\u00a05701, pp. 294\u2013309. Springer, Heidelberg (2009)"},{"issue":"3","key":"5_CR22","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods in System Design\u00a019(3), 291\u2013314 (2001)","journal-title":"Formal Methods in System Design"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal verification of reactive systems - safety. Springer (1995)","DOI":"10.1007\/978-1-4612-4222-2"},{"issue":"3","key":"5_CR24","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":"5_CR25","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":"5_CR26","doi-asserted-by":"crossref","unstructured":"Snodgrass, R.T. (ed.): The TSQL2 Temporal Query Language. Kluwer (1995)","DOI":"10.1007\/978-1-4615-2289-8"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Toman, D.: Expiration of historical databases. In: TIME, pp. 128\u2013135 (2001)","DOI":"10.1109\/TIME.2001.930708"},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency","author":"M.Y. Vardi","year":"1996","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol.\u00a01043, pp. 238\u2013266. Springer, Heidelberg (1996)"}],"container-title":["Lecture Notes in Computer Science","Service-Oriented Computing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-45005-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T23:52:08Z","timestamp":1746057128000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-45005-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642173578","9783642173585"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-45005-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}