{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:40:50Z","timestamp":1742913650021,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662457290"},{"type":"electronic","value":"9783662457306"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-45730-6_6","type":"book-chapter","created":{"date-parts":[[2014,12,2]],"date-time":"2014-12-02T17:08:59Z","timestamp":1417540139000},"page":"99-123","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Symbolic Termination and Confluence Checking for ECA Rules"],"prefix":"10.1007","author":[{"given":"Xiaoqing","family":"Jin","sequence":"first","affiliation":[]},{"given":"Yousra","family":"Lembachar","sequence":"additional","affiliation":[]},{"given":"Gianfranco","family":"Ciardo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,12,3]]},"reference":[{"issue":"2","key":"6_CR1","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/s00778-003-0095-z","volume":"12","author":"DJ Abadi","year":"2003","unstructured":"Abadi, D.J., Carney, D., \u00c7etintemel, U., Cherniack, M., Convey, C., Lee, S., Stonebraker, M., Tatbul, N., Zdonik, S.: Aurora: a new model and architecture for data stream management. VLDB J. 12(2), 120\u2013139 (2003)","journal-title":"VLDB J."},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Aiken, A., Widom, J., Hellerstein, J.M.: Behavior of database production rules: termination, confluence, and observable determinism. In: Proceedings of the ACM SIGMOD International Conference on Management of Data, pp. 59\u201368. ACM Press (1992)","DOI":"10.1145\/141484.130296"},{"key":"6_CR3","unstructured":"Augusto, J.C., Nugent, C.D.: A new architecture for smart homes based on ADB and temporal reasoning. In: Toward a Human-Friendly Assistive Environment, vol. 14, pp. 106\u2013113 (2004)"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/3-540-60365-4_126","volume-title":"Rules in Database Systems","author":"E Baralis","year":"1995","unstructured":"Baralis, E., Ceri, S., Paraboschi, S.: Improved rule analysis by means of triggering and activation graphs. In: Sellis, T.K. (ed.) RIDS 1995. LNCS, vol. 985, pp. 163\u2013181. Springer, Heidelberg (1995)"},{"issue":"3","key":"6_CR5","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1145\/363951.363954","volume":"25","author":"E Baralis","year":"2000","unstructured":"Baralis, E., Widom, J.: An algebraic approach to static analysis of active database rules. ACM Trans. Database Syst. 25(3), 269\u2013332 (2000)","journal-title":"ACM Trans. Database Syst."},{"issue":"8","key":"6_CR6","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"6_CR7","doi-asserted-by":"publisher","first-page":"826","DOI":"10.2197\/ipsjdc.2.826","volume":"2","author":"E-H Choi","year":"2006","unstructured":"Choi, E.-H., Tsuchiya, T., Kikuno, T.: Model checking active database rules under various rule processing strategies. IPSJ Digit. Cour. 2, 826\u2013839 (2006)","journal-title":"IPSJ Digit. Cour."},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-540-45232-4_6","volume-title":"Computer Performance Evaluations. Modelling Techniques and Tools","author":"G Ciardo","year":"2003","unstructured":"Ciardo, G., Jones, R.L., Miner, A.S., Siminiceanu, R.I.: Logical and stochastic modeling with Smart. In: Kemper, P., Sanders, W.H. (eds.) TOOLS 2003. LNCS, vol. 2794, pp. 78\u201397. Springer, Heidelberg (2003)"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/3-540-45319-9_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Ciardo","year":"2001","unstructured":"Ciardo, G., L\u00fcttgen, G., Siminiceanu, R.I.: Saturation: an efficient iteration strategy for symbolic state-space generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 328\u2013342. Springer, Heidelberg (2001)"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-29072-5_3","volume-title":"Transactions on Petri Nets and Other Models of Concurrency V","author":"G Ciardo","year":"2012","unstructured":"Ciardo, G., Zhao, Y., Jin, X.: Ten years of saturation: a petri net perspective. In: Jensen, K., Donatelli, S., Kleijn, J. (eds.) ToPNoC V. LNCS, vol. 6900, pp. 51\u201395. Springer, Heidelberg (2012)"},{"key":"6_CR11","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"6_CR12","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1109\/TKDE.2003.1185831","volume":"15","author":"S Comai","year":"2003","unstructured":"Comai, S., Tanca, L.: Termination and confluence by rule prioritization. IEEE Trans. Knowl. Data Eng. 15, 257\u2013270 (2003)","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"crossref","first-page":"352","DOI":"10.1007\/978-3-540-24581-0_30","volume-title":"AI 2003: Advances in Artificial Intelligence","author":"T French","year":"2003","unstructured":"French, T.: Decidability of propositionally quantified logics of knowledge. In: Gedeon, T.T.D., Fung, L.C.C. (eds.) AI 2003. LNCS (LNAI), vol. 2903, pp. 352\u2013363. Springer, Heidelberg (2003)"},{"issue":"1\u20132","key":"6_CR14","first-page":"9","volume":"4","author":"T Kam","year":"1998","unstructured":"Kam, T., Villa, T., Brayton, R.K., Sangiovanni-Vincentelli, A.: Multi-valued decision diagrams: theory and applications. Multiple-Valued Logic 4(1\u20132), 9\u201362 (1998)","journal-title":"Multiple-Valued Logic"},{"key":"6_CR15","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-1-4419-8656-6_10","volume-title":"Active Rules in Database Systems","author":"KG Kulkarni","year":"1999","unstructured":"Kulkarni, K.G., Mattos, N.M., Cochrane, R.: Active database features in SQL3. In: Paton, N.W. (ed.) Active Rules in Database Systems, pp. 197\u2013219. Springer, New York (1999)"},{"key":"6_CR16","unstructured":"Lee, E.A.: Computing foundations and practice for cyber-physical systems: a preliminary report. Technical report UCB\/EECS-2007-72, University of California, Berkeley, May 2007"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","first-page":"486","volume-title":"MICAI 2002: Advances in Artificial Intelligence","author":"X Li","year":"2002","unstructured":"Li, X., Medina Mar\u00edn, J., Chapa, S.V.: A structural model of ECA rules in active database. In: Coello Coello, C.A., de Albornoz, \u00c1., Sucar, L.E., Battistutti, O.C. (eds.) MICAI 2002. LNCS (LNAI), vol. 2313, pp. 486\u2013493. Springer, Heidelberg (2002)"},{"issue":"2","key":"6_CR18","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1145\/66926.66946","volume":"18","author":"D McCarthy","year":"1989","unstructured":"McCarthy, D., Dayal, U.: The architecture of an active database management system. ACM Sigmod Rec. 18(2), 215\u2013224 (1989)","journal-title":"ACM Sigmod Rec."},{"issue":"4","key":"6_CR19","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata, T.: Petri nets: properties, analysis and applications. Proc. of the IEEE 77(4), 541\u2013579 (1989)","journal-title":"Proc. of the IEEE"},{"issue":"3","key":"6_CR20","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1109\/69.224193","volume":"5","author":"D Nazareth","year":"1993","unstructured":"Nazareth, D.: Investigating the applicability of petri nets for rule-based system verification. IEEE Trans. Knowl. Data Eng. 5(3), 402\u2013415 (1993)","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"6_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/3-540-44803-9_21","volume-title":"Advances in Databases and Information Systems","author":"I Ray","year":"2001","unstructured":"Ray, I., Ray, I.: Detecting termination of active database rules using symbolic model checking. In: Caplinskas, A., Eder, J. (eds.) ADBIS 2001. LNCS, vol. 2151, pp. 266\u2013279. Springer, Heidelberg (2001)"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/3-540-10856-4_80","volume-title":"Mathematical Foundations of Computer Science 1981","author":"R Valk","year":"1981","unstructured":"Valk, R.: Generalizations of petri nets. In: Gruska, J., Chytil, M.P. (eds.) MFCS 1981. LNCS, vol. 118, pp. 140\u2013155. Springer, Heidelberg (1981)"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-45832-8_28","volume-title":"Graph Transformation","author":"D Varr\u00f3","year":"2002","unstructured":"Varr\u00f3, D.: A formal semantics of uml statecharts by model transition systems. In: Corradini, A., Ehrig, H., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2002. LNCS, vol. 2505, pp. 378\u2013392. Springer, Heidelberg (2002)"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-642-04761-9_27","volume-title":"Automated Technology for Verification and Analysis","author":"Y Zhao","year":"2009","unstructured":"Zhao, Y., Ciardo, G.: Symbolic CTL model checking of asynchronous systems using constrained saturation. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 368\u2013381. Springer, Heidelberg (2009)"},{"issue":"2","key":"6_CR25","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/s11334-011-0146-3","volume":"7","author":"Y Zhao","year":"2011","unstructured":"Zhao, Y., Ciardo, G.: Symbolic computation of strongly connected components and fair cycles using saturation. Innov. Syst. Softw. Eng. 7(2), 141\u2013150 (2011)","journal-title":"Innov. Syst. Softw. Eng."},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Zhao, Y., Xiaoqing, J., Ciardo, G.: A symbolic algorithm for shortest EG witness generation. In: Proceedings of TASE, pp. 68\u201375. IEEE Computer Society Press (2011)","DOI":"10.1109\/TASE.2011.35"}],"container-title":["Lecture Notes in Computer Science","Transactions on Petri Nets and Other Models of Concurrency IX"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-45730-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T02:26:46Z","timestamp":1676428006000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-45730-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662457290","9783662457306"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-45730-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"3 December 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}