{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T07:05:55Z","timestamp":1794380755522,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642153839","type":"print"},{"value":"9783642153846","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15384-6_15","type":"book-chapter","created":{"date-parts":[[2010,9,5]],"date-time":"2010-09-05T07:24:42Z","timestamp":1283671482000},"page":"135-144","source":"Crossref","is-referenced-by-count":1,"title":["ACTL Local Model Update with Constraints"],"prefix":"10.1007","author":[{"given":"Michael","family":"Kelly","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fei","family":"Pu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yan","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yi","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04558-9","volume-title":"System and Software Verification: Model-Checking techniques and tools","author":"B. Berard","year":"2001","unstructured":"Berard, B., et al.: System and Software Verification: Model-Checking techniques and tools. Springer, Heidelberg (2001)"},{"key":"15_CR2","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1006\/jcss.2000.1734","volume":"62","author":"F. Buccafurri","year":"2001","unstructured":"Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: On ACTL formulas having linear counterexamples. Journal of Computer and System Sciences\u00a062, 463\u2013515 (2001)","journal-title":"Journal of Computer and System Sciences"},{"key":"15_CR3","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/S0004-3702(99)00039-9","volume":"112","author":"F. Buccafurri","year":"1999","unstructured":"Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: Enhancing model checking in verification by AI techniques. Artificial Intelligence\u00a0112, 57\u2013104 (1999)","journal-title":"Artificial Intelligence"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Clarke Jr., E., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 19\u201329 (2002)","DOI":"10.1109\/LICS.2002.1029814"},{"key":"15_CR5","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E. Clarke Jr.","year":"2003","unstructured":"Clarke Jr., E., Grumberg, O., Jha, S., Liu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. Journal of ACM\u00a050, 752\u2013794 (2003)","journal-title":"Journal of ACM"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Fraser, G., Wotawa, F.: Nondeterministic testing with linear model-checking counterexamples. In: Proceedings of the 7th Intel. Conf on Quality Software, QSIC 2007 (2007)","DOI":"10.1109\/QSIC.2007.4385486"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Harris, H., Ryan, M.: Theoretical foundations of updating systems. In: Proceedings of the 18th IEEE International Conference on Automated Software Engineering, pp. 291\u2013298 (2003)","DOI":"10.1109\/ASE.2003.1240323"},{"key":"15_CR8","doi-asserted-by":"crossref","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, 2nd edn. Cambridge University Press, Cambridge (2004)","edition":"2"},{"key":"15_CR9","unstructured":"Jobstmann, B., Staber, S., Griesmayer, A., Bloem, R.: Finding and fixing faults. Journal of Computer and System Sciences (2010) (to appear)"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Kelly, M., Zhang, Y., Zhou, Y.: Local model update with an application to sliding window protocol (2010) (under review)","DOI":"10.1007\/978-3-642-15384-6_2"},{"key":"15_CR11","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1613\/jair.2420","volume":"31","author":"Y. Zhang","year":"2008","unstructured":"Zhang, Y., Ding, Y.: CTL model update for system modifications. Journal of Artificial Intelligence Research\u00a031, 113\u2013155 (2008)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Zhang, Y., Kelly, M., Zhou, Y.: Foundations of tree-like local model updates (2010) (under review)","DOI":"10.3233\/978-1-60750-606-5-615"}],"container-title":["Lecture Notes in Computer Science","Knowledge-Based and Intelligent Information and Engineering Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15384-6_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T10:24:34Z","timestamp":1740479074000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15384-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642153839","9783642153846"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15384-6_15","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-642-15384-6","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}