{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:22:13Z","timestamp":1740122533115,"version":"3.37.3"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T00:00:00Z","timestamp":1659744000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T00:00:00Z","timestamp":1659744000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100001807","name":"Funda\u00e7\u00e3o de Amparo \u00e1 Pesquisa do Estado de S\u00e3o Paulo","doi-asserted-by":"publisher","award":["2010\/15392-3"],"award-info":[{"award-number":["2010\/15392-3"]}],"id":[{"id":"10.13039\/501100001807","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003593","name":"Conselho Nacional de Desenvolvimento Cient\u00edfico e Tecnol\u00f3gico","doi-asserted-by":"publisher","award":["447178\/2014-8"],"award-info":[{"award-number":["447178\/2014-8"]}],"id":[{"id":"10.13039\/501100003593","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J of Log Lang and Inf"],"published-print":{"date-parts":[[2022,12]]},"DOI":"10.1007\/s10849-022-09376-9","type":"journal-article","created":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T08:02:37Z","timestamp":1659772957000},"page":"591-618","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Revising System Specifications in Temporal Logic"],"prefix":"10.1007","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0424-055X","authenticated-orcid":false,"given":"Paulo T.","family":"Guerra","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8065-1433","authenticated-orcid":false,"given":"Renata","family":"Wassermann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,6]]},"reference":[{"issue":"2","key":"9376_CR1","doi-asserted-by":"publisher","first-page":"510","DOI":"10.2307\/2274239","volume":"50","author":"CE Alchourron","year":"1985","unstructured":"Alchourron, C. E., G\u00e4rdenfors, P., & Makinson, D. (1985). On the logic of theory change: Partial meet contraction and revision functions. Journal of Symbolic Logic, 50(2), 510\u2013530.","journal-title":"Journal of Symbolic Logic"},{"issue":"1","key":"9376_CR2","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1111\/j.1755-2567.1982.tb00480.x","volume":"48","author":"CE Alchourron","year":"1982","unstructured":"Alchourron, C. E., & Makinson, D. (1982). On the logic of theory change: Contraction functions and their associated revision functions. Theoria, 48(1), 14\u201337. https:\/\/doi.org\/10.1111\/j.1755-2567.1982.tb00480.x","journal-title":"Theoria"},{"key":"9376_CR3","doi-asserted-by":"publisher","unstructured":"Baier, C., & Katoen, J. P. (2008). Principles of model checking. MIT Press. https:\/\/doi.org\/10.1093\/comjnl\/bxp025","DOI":"10.1093\/comjnl\/bxp025"},{"issue":"1\u20132","key":"9376_CR4","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. (1999). Enhancing model checking in verification by AI techniques. Artificial Intelligence, 112(1\u20132), 57\u2013104. https:\/\/doi.org\/10.1016\/S0004-3702(99)00039-9","journal-title":"Artificial Intelligence"},{"issue":"2","key":"9376_CR5","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J Burch","year":"1992","unstructured":"Burch, J., Clarke, E., McMillan, K., Dill, D., & Hwang, L. (1992). Symbolic model checking: $$10^{20}$$ States and Beyond. Information and Computation, 98(2), 142\u2013170. https:\/\/doi.org\/10.1016\/0890-5401(92)90017-A","journal-title":"Information and Computation"},{"key":"9376_CR6","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-642-28891-3_32","volume-title":"NASA formal methods. Lecture notes in computer science","author":"G Chatzieleftheriou","year":"2012","unstructured":"Chatzieleftheriou, G., Bonakdarpour, B., Smolka, S. A., & Katsaros, P. (2012). Abstract model repair. In A. Goodloe & S. Person (Eds.), NASA formal methods. Lecture notes in computer science (Vol. 7226, pp. 341\u2013355). Springer. https:\/\/doi.org\/10.1007\/978-3-642-28891-3_32"},{"key":"9376_CR7","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of programs. Lecture notes in computer science","author":"EM Clarke","year":"1982","unstructured":"Clarke, E. M., & Emerson, E. A. (1982). Design and synthesis of synchronization skeletons using branching time temporal logic. In D. Kozen (Ed.), Logics of programs. Lecture notes in computer science (Vol. 131, pp. 52\u201371). Springer. https:\/\/doi.org\/10.1007\/BFb0025774"},{"issue":"2","key":"9376_CR8","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke, E. M., Emerson, E. A., & Sistla, A. P. (1986). Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS), 8(2), 244\u2013263. https:\/\/doi.org\/10.1145\/5397.5399","journal-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"9376_CR9","volume-title":"Model checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E. M., Grumberg, O., & Peled, D. A. (1999). Model checking. Springer."},{"key":"9376_CR10","doi-asserted-by":"publisher","DOI":"10.4324\/9780203028100","volume-title":"A new introduction to modal logic","author":"MJ Cresswell","year":"2012","unstructured":"Cresswell, M. J., & Hughes, G. E. (2012). A new introduction to modal logic. Routledge."},{"key":"9376_CR11","doi-asserted-by":"crossref","unstructured":"Finger, M., & Wassermann, R. (2008). Revising specifications with CTL properties using bounded model checking. In Proceedings of the 19th Brazilian symposium on artificial intelligence (SBIA\u201908), Lecture notes in artificial intelligence (Vol. 5249, pp. 157\u2013166). Springer.","DOI":"10.1007\/978-3-540-88190-2_21"},{"issue":"2","key":"9376_CR12","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/BF00247909","volume":"17","author":"A Grove","year":"1988","unstructured":"Grove, A. (1988). Two modellings for theory change. Journal of Philosophical Logic, 17(2), 157\u2013170. https:\/\/doi.org\/10.1007\/BF00247909","journal-title":"Journal of Philosophical Logic"},{"key":"9376_CR13","unstructured":"Guerra, P. T. (2010). Revis\u00e3o de Modelos CTL. Master\u2019s thesis, Universidade de S\u00e3o Paulo."},{"key":"9376_CR14","first-page":"115","volume-title":"Formal methods: Foundations and applications. 16th Brazilian symposium on formal methods (SBMF 2013), Lecture notes in computer science","author":"PT Guerra","year":"2013","unstructured":"Guerra, P. T., Andrade, A., & Wassermann, R. (2013). Toward the revision of CTL models through Kripke modal transition systems. In J. Iyoda & L. M. de Moura (Eds.), Formal methods: Foundations and applications. 16th Brazilian symposium on formal methods (SBMF 2013), Lecture notes in computer science (Vol. 8195, pp. 115\u2013130). Springer."},{"key":"9376_CR15","first-page":"153","volume-title":"Advances in artificial intelligence\u2014IBERAMIA 2010, LNCS","author":"PT Guerra","year":"2010","unstructured":"Guerra, P. T., & Wassermann, R. (2010). Revision of CTL models. In A. Kuri-Morales & G. Simari (Eds.), Advances in artificial intelligence\u2014IBERAMIA 2010, LNCS (Vol. 6433, pp. 153\u2013162). Springer."},{"key":"9376_CR16","unstructured":"Guerra, P. T., & Wassermann, R. (2017). On the uncomputability of partial meet contraction for linear-time temporal logic. In Brazilian logic meeting\u2014Book of abstracts. Extended version accepted for publication in the South American Journal of Logic, 2019."},{"key":"9376_CR17","unstructured":"Guerra, P. T., Wassermann, R. (2018). Two AGM-style characterizations of model repair. In Proceedings of the 16th international conference on principles of knowledge representation and reasoning (KR 2018) (pp. 645\u2013646)."},{"key":"9376_CR18","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-0814-3","volume-title":"A textbook of belief dynamics. Theory change and database updating","author":"SO Hansson","year":"1999","unstructured":"Hansson, S. O. (1999). A textbook of belief dynamics. Theory change and database updating. Kluwer Academic."},{"issue":"1","key":"9376_CR19","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1023\/A:1014654208944","volume":"70","author":"SO Hansson","year":"2002","unstructured":"Hansson, S. O., & Wassermann, R. (2002). Local change. Studia Logica, 70(1), 49\u201376.","journal-title":"Studia Logica"},{"issue":"1","key":"9376_CR20","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/S0004-3702(99)00072-7","volume":"115","author":"A Herzig","year":"1999","unstructured":"Herzig, A., & Rifi, O. (1999). Propositional belief base update and minimal change. Artificial Intelligence, 115(1), 107\u2013138. https:\/\/doi.org\/10.1016\/S0004-3702(99)00072-7","journal-title":"Artificial Intelligence"},{"key":"9376_CR21","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/3-540-47813-2_21","volume-title":"Verification, model checking, and abstract interpretation","author":"M Huth","year":"2002","unstructured":"Huth, M. (2002). Model checking modal transition systems using Kripke structures. In A. Cortesi (Ed.), Verification, model checking, and abstract interpretation (pp. 302\u2013316). Springer."},{"key":"9376_CR22","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-45309-1_11","volume-title":"Programming languages and systems. Lecture notes in computer science","author":"M Huth","year":"2001","unstructured":"Huth, M., Jagadeesan, R., & Schmidt, D. (2001). Modal transition systems: A foundation for three-valued program analysis. In D. Sands (Ed.), Programming languages and systems. Lecture notes in computer science (Vol. 2028, pp. 155\u2013169). Springer. https:\/\/doi.org\/10.1007\/3-540-45309-1_11"},{"key":"9376_CR23","unstructured":"Katsuno, H., & Mendelzon, A. O. (1991). On the difference between updating a knowledge base and revising it. In Proceedings of the second international conference on principles of knowledge representation and reasoning (KR\u201991) (pp. 387\u2013395). Morgan Kaufmann."},{"issue":"3","key":"9376_CR24","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. (1983). Results on the propositional $$\\mu $$-calculus. Theoretical Computer Science, 27(3), 333\u2013354. https:\/\/doi.org\/10.1016\/0304-3975(82)90125-6","journal-title":"Theoretical Computer Science"},{"key":"9376_CR25","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-52148-8_19","volume-title":"Automatic verification methods for finite state systems. Lecture notes in computer science","author":"KG Larsen","year":"1990","unstructured":"Larsen, K. G. (1990). Modal specifications. In J. Sifakis (Ed.), Automatic verification methods for finite state systems. Lecture notes in computer science (Vol. 407, pp. 232\u2013246). Springer."},{"key":"9376_CR26","doi-asserted-by":"publisher","unstructured":"Larsen, K. G., & Thomsen, B. (1988). A modal process logic. In Proceedings of the third annual symposium on logic in computer science, 1988. LICS \u201988 (pp. 203\u2013210). https:\/\/doi.org\/10.1109\/LICS.1988.5119","DOI":"10.1109\/LICS.1988.5119"},{"key":"9376_CR27","doi-asserted-by":"publisher","unstructured":"Pnueli, A. (1977). The temporal logic of programs. In Proceedings of the 18th annual symposium on foundations of computer science, SFCS\u201977 (pp. 46\u201357). IEEE Computer Society. https:\/\/doi.org\/10.1109\/SFCS.1977.32.","DOI":"10.1109\/SFCS.1977.32"},{"key":"9376_CR28","doi-asserted-by":"crossref","unstructured":"Queille, J. P., & Sifakis, J. (1982). Specification and verification of concurrent systems in CESAR. In Proceedings of the 5th colloquium on international symposium on programming (pp. 337\u2013351). Springer. http:\/\/dl.acm.org\/citation.cfm?id=647325.721668","DOI":"10.1007\/3-540-11494-7_22"},{"key":"9376_CR29","unstructured":"Ribeiro, J., Nayak, A., & Wassermann, R. (2018). Towards belief contraction without compactness. In Knowledge representation and reasoning conference (KR) (pp. 287\u2013296)."},{"key":"9376_CR30","doi-asserted-by":"crossref","unstructured":"Ribeiro, J. S., & Andrade, A. (2015). A 3-valued contraction model checking game: Deciding on the world of partial information. In Formal methods and software engineering\u2014Proceedings of the 17th international conference on formal engineering methods, ICFEM 2015 (pp. 84\u201399).","DOI":"10.1007\/978-3-319-25423-4_6"},{"key":"9376_CR31","unstructured":"Sousa, T. C., & Wassermann, R. (2007). Handling inconsistencies in CTL model-checking using belief revision. In Proc. of the Brazilian symposium on formal methods."},{"key":"9376_CR32","unstructured":"Van Zee, M., Doder, D., Dastani, M., & Van Der Torre, L. (2015). AGM revision of beliefs about action and time. In Proc. international conference on artificial intelligence (pp. 3250\u20133256). AAAI Press. http:\/\/dl.acm.org\/citation.cfm?id=2832581.2832702"},{"issue":"1","key":"9376_CR33","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1613\/jair.2420","volume":"31","author":"Y Zhang","year":"2008","unstructured":"Zhang, Y., & Ding, Y. (2008). CTL model update for system modifications. Journal of Artificial Intelligence Research, 31(1), 113\u2013155.","journal-title":"Journal of Artificial Intelligence Research"}],"container-title":["Journal of Logic, Language and Information"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10849-022-09376-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10849-022-09376-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10849-022-09376-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,4]],"date-time":"2022-12-04T06:03:49Z","timestamp":1670133829000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10849-022-09376-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,6]]},"references-count":33,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["9376"],"URL":"https:\/\/doi.org\/10.1007\/s10849-022-09376-9","relation":{},"ISSN":["0925-8531","1572-9583"],"issn-type":[{"type":"print","value":"0925-8531"},{"type":"electronic","value":"1572-9583"}],"subject":[],"published":{"date-parts":[[2022,8,6]]},"assertion":[{"value":"5 July 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 August 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no conflict of interest.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}},{"value":"This work does not contain any studies with human participants or animals performed by any of the authors.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical Approval"}}]}}