{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T02:47:17Z","timestamp":1725677237024},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540881896"},{"type":"electronic","value":"9783540881902"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-88190-2_21","type":"book-chapter","created":{"date-parts":[[2008,10,16]],"date-time":"2008-10-16T11:54:19Z","timestamp":1224158059000},"page":"157-166","source":"Crossref","is-referenced-by-count":3,"title":["Revising Specifications with CTL Properties Using Bounded Model Checking"],"prefix":"10.1007","author":[{"given":"Marcelo","family":"Finger","sequence":"first","affiliation":[]},{"given":"Renata","family":"Wassermann","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"5","key":"21_CR1","first-page":"689","volume":"3","author":"K. Winter","year":"1997","unstructured":"Winter, K.: Model checking for abstract state machines. Journal of Universal Computer Science\u00a03(5), 689\u2013701 (1997)","journal-title":"Journal of Universal Computer Science"},{"key":"21_CR2","unstructured":"B\u00fcessow, R.: Model Checking Combined Z and Statechart Specifications. PhD thesis, Technical University of Berlin, Faculty of Computer Science (November 2003), \n                    \n                      http:\/\/edocs.tu-berlin.de\/diss\/2003\/buessow_robert.pdf"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M. Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: A model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol.\u00a02805, pp. 855\u2013874. Springer, Heidelberg (2003)"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/BFb0105411","volume-title":"Theorem Proving in Higher Order Logics","author":"S.T. Kolyang","year":"1996","unstructured":"Kolyang, S.T., Wolff, B.: A structure preserving encoding of Z in Isabelle\/HOL. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 283\u2013298. Springer, Heidelberg (1996)"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/3-540-58179-0_72","volume-title":"Computer Aided Verification","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 415\u2013427. Springer, Heidelberg (1994)"},{"key":"21_CR6","unstructured":"de Sousa, T.C., Wassermann, R.: Handling inconsistencies in CTL model-checking using belief revision. In: Proceedings of the Brazilian Symposium on Formal Methods (SBMF) (2007)"},{"key":"21_CR7","volume-title":"Knowledge in Flux: Modeling the Dynamics of Epistemic States","author":"P. G\u00e4rdenfors","year":"1988","unstructured":"G\u00e4rdenfors, P.: Knowledge in Flux: Modeling the Dynamics of Epistemic States. MIT Press, Cambridge (1988)"},{"key":"21_CR8","volume-title":"A Textbook of Belief Dynamics","author":"S.O. Hansson","year":"1997","unstructured":"Hansson, S.O.: A Textbook of Belief Dynamics. Kluwer Academic Publishers, Dordrecht (1997)"},{"issue":"1","key":"21_CR9","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1023\/A:1014654208944","volume":"70","author":"S.O. Hansson","year":"2002","unstructured":"Hansson, S.O., Wassermann, R.: Local change. Studia Logica\u00a070(1), 49\u201376 (2002)","journal-title":"Studia Logica"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without bdds. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"issue":"2","key":"21_CR11","doi-asserted-by":"publisher","first-page":"510","DOI":"10.2307\/2274239","volume":"50","author":"C. Alchourr\u00f3n","year":"1985","unstructured":"Alchourr\u00f3n, C., G\u00e4rdenfors, P., Makinson, D.: On the logic of theory change: Partial meet contraction and revision functions. Journal of Symbolic Logic\u00a050(2), 510\u2013530 (1985)","journal-title":"Journal of Symbolic Logic"},{"issue":"2","key":"21_CR12","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/BF00247909","volume":"17","author":"A. Grove","year":"1988","unstructured":"Grove, A.: Two modellings for theory change. Journal of Philosophical Logic\u00a017(2), 157\u2013170 (1988)","journal-title":"Journal of Philosophical Logic"},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"21_CR14","volume-title":"Logic in Computer Science: Modelling and Reasoning about Systems","author":"M. Huth","year":"2000","unstructured":"Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, Cambridge (2000)"},{"key":"21_CR15","unstructured":"Flouris, G.: On Belief Change and Ontology Evolution. PhD thesis, University of Crete (2006)"},{"issue":"1","key":"21_CR16","first-page":"135","volume":"51","author":"W. Penczek","year":"2002","unstructured":"Penczek, W., Wozna, B., Zbrzezny, A.: Bounded model checking for the universal fragment of CTl. Fundamenta Informaticae\u00a051(1), 135\u2013156 (2002)","journal-title":"Fundamenta Informaticae"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of the 38th Design Automation Conference (DAC 2001), pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: Berkmin: A Fast and Robust SAT Solver. In: Design Automation and Test in Europe (DATE 2002), pp. 142\u2013149 (2002)","DOI":"10.1109\/DATE.2002.998262"}],"container-title":["Lecture Notes in Computer Science","Advances in Artificial Intelligence - SBIA 2008"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88190-2_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,3]],"date-time":"2019-03-03T18:48:11Z","timestamp":1551638891000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88190-2_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540881896","9783540881902"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88190-2_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}