{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T13:22:36Z","timestamp":1725974556600},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319901039"},{"type":"electronic","value":"9783319901046"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-90104-6_5","type":"book-chapter","created":{"date-parts":[[2018,4,17]],"date-time":"2018-04-17T12:53:22Z","timestamp":1523969602000},"page":"69-87","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["The Complexity of Linear-Time Temporal Logic Model Repair"],"prefix":"10.1007","author":[{"given":"Xiuting","family":"Tao","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guoqiang","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,18]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/3-540-45988-X_13","volume-title":"Frontiers of Combining Systems","author":"P Balbiani","year":"2002","unstructured":"Balbiani, P., Jean-Fran\u00e7ois, C.: Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning. In: Armando, A. (ed.) FroCoS 2002. LNCS (LNAI), vol. 2309, pp. 162\u2013176. Springer, Heidelberg (2002). \nhttps:\/\/doi.org\/10.1007\/3-540-45988-X_13"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-71389-0_5","volume-title":"Foundations of Software Science and Computational Structures","author":"M Bauland","year":"2007","unstructured":"Bauland, M., Schneider, T., Schnoor, H., Schnoor, I., Vollmer, H.: The complexity of generalized satisfiability for linear temporal logic. In: Seidl, H. (ed.) FoSSaCS 2007. LNCS, vol. 4423, pp. 48\u201362. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71389-0_5"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/3-540-48683-6_25","volume-title":"Computer Aided Verification","author":"G Bruns","year":"1999","unstructured":"Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274\u2013287. Springer, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/3-540-48683-6_25"},{"issue":"1","key":"5_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.: Enhancing model checking in verification by AI techniques. Artif. Intell. 112(1), 57\u2013104 (1999)","journal-title":"Artif. Intell."},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/10722167_34","volume-title":"Computer Aided Verification","author":"W Chan","year":"2000","unstructured":"Chan, W.: Temporal-logic queries. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 450\u2013463. Springer, Heidelberg (2000). \nhttps:\/\/doi.org\/10.1007\/10722167_34"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM 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. 131, pp. 52\u201371. Springer, Heidelberg (1982). \nhttps:\/\/doi.org\/10.1007\/BFb0025774"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). \nhttps:\/\/doi.org\/10.1007\/10722167_15"},{"key":"5_CR8","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, London (1999)"},{"key":"5_CR9","unstructured":"Dasgupta, S., Papadimitriou, C.H., Vazirani, U.V.: Algorithms (2016)"},{"issue":"1","key":"5_CR10","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: Sometimes and not never revisited: on branching versus linear time temporal logic. J. ACM (JACM) 33(1), 151\u2013178 (1986)","journal-title":"J. ACM (JACM)"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-319-04921-2_29","volume-title":"Language and Automata Theory and Applications","author":"B Finkbeiner","year":"2014","unstructured":"Finkbeiner, B., Torfah, H.: Counting models of linear-time temporal logic. In: Dediu, A.-H., Mart\u00edn-Vide, C., Sierra-Rodr\u00edguez, J.-L., Truthe, B. (eds.) LATA 2014. LNCS, vol. 8370, pp. 360\u2013371. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-04921-2_29"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 163\u2013173. ACM (1980)","DOI":"10.1145\/567446.567462"},{"issue":"3","key":"5_CR13","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10009-005-0202-0","volume":"8","author":"A Groce","year":"2006","unstructured":"Groce, A., Chaki, S., Kroening, D., Strichman, O.: Error explanation with distance metrics. Int. J. Softw. Tools Technol. Transf. (STTT) 8(3), 229\u2013247 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"5_CR14","doi-asserted-by":"publisher","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. Cambridge University Press, Cambridge (2004)"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 97\u2013107. ACM (1985)","DOI":"10.1145\/318593.318622"},{"key":"5_CR16","unstructured":"Mateis, C., Stumptner, M., Wotawa, F.: A value-based diagnosis model for Java programs (2000)"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"1","key":"5_CR18","first-page":"19","volume":"3","author":"M Reynolds","year":"2010","unstructured":"Reynolds, M.: The complexity of decision problems for linear temporal logics. J. Stud. Logic 3(1), 19\u201350 (2010)","journal-title":"J. Stud. Logic"},{"issue":"393\u2013436","key":"5_CR19","first-page":"35","volume":"4","author":"P Schnoebelen","year":"2002","unstructured":"Schnoebelen, P.: The complexity of temporal logic model checking. Adv. Modal Logic 4(393\u2013436), 35 (2002)","journal-title":"Adv. Modal Logic"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Xiang, J., Machida, F., Tadano, K., Yanoo, K., Sun, W., Maeno, Y.: A static analysis of dynamic fault trees with priority-and gates. In: 2013 Sixth Latin-American Symposium on Dependable Computing (LADC), pp. 58\u201367. IEEE (2013)","DOI":"10.1109\/LADC.2013.14"}],"container-title":["Lecture Notes in Computer Science","Structured Object-Oriented Formal Language and Method"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-90104-6_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,4,17]],"date-time":"2018-04-17T12:55:51Z","timestamp":1523969751000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-90104-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319901039","9783319901046"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-90104-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}