{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T07:18:32Z","timestamp":1775027912618,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540781622","type":"print"},{"value":"9783540781639","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78163-9_9","type":"book-chapter","created":{"date-parts":[[2008,2,29]],"date-time":"2008-02-29T10:30:06Z","timestamp":1204281006000},"page":"52-67","source":"Crossref","is-referenced-by-count":52,"title":["Diagnostic Information for Realizability"],"prefix":"10.1007","author":[{"given":"A.","family":"Cimatti","sequence":"first","affiliation":[]},{"given":"M.","family":"Roveri","sequence":"additional","affiliation":[]},{"given":"V.","family":"Schuppan","sequence":"additional","affiliation":[]},{"given":"A.","family":"Tchaltsev","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0035748","volume-title":"Automata, Languages and Programming","author":"M. Abadi","year":"1989","unstructured":"Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol.\u00a0372, pp. 1\u201317. Springer, Heidelberg (1989)"},{"key":"9_CR2","unstructured":"European\u00a0Railway Agency. Feasibility study for the formal specification of ETCS functions. Sep, Invitation to tender (2007), http:\/\/www.era.europa.eu"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Behrmann, G., et al.: UPPAAL-Tiga: Time for playing games! In: Damm and Hermanns [11], pp. 121\u2013125.","DOI":"10.1007\/978-3-540-73368-3_14"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Bloem, R., et al.: RAT: Formal analysis of requirements. In: Damm and Hermanns [11], pp. 263\u2013267.","DOI":"10.1007\/978-3-540-73368-3_30"},{"key":"9_CR5","first-page":"1188","volume-title":"DATE","author":"R. Bloem","year":"2007","unstructured":"Bloem, R., et al.: Interactive presentation: Automatic hardware synthesis from specifications: A case study. In: Lauwereins, R., Madsen, J. (eds.) DATE, pp. 1188\u20131193. ACM Press, New York (2007)"},{"issue":"2","key":"9_CR6","first-page":"139","volume":"62","author":"Y. Bontemps","year":"2004","unstructured":"Bontemps, Y., Schobbens, P., L\u00f6ding, C.: Synthesis of open reactive systems from scenario-based specifications. Fundam. Inform.\u00a062(2), 139\u2013169 (2004)","journal-title":"Fundam. Inform."},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","first-page":"495","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., et al.: NuSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 495\u2013499. Springer, Heidelberg (1999)"},{"key":"9_CR8","unstructured":"Cimatti, A., et al.: Diagnostic information for realizability. Technical Report FBK-092007-01, Fondazione Bruno Kessler (2007), http:\/\/es.fbk.eu\/people\/roveri\/tests\/vmcai08"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Cimatti, A., et al.: Boolean abstraction for temporal logic satisfiability. In: Damm and Hermanns [11], pp. 532\u2013546","DOI":"10.1007\/978-3-540-73368-3_53"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","first-page":"208","volume-title":"Verification: Theory and Practice","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Veith, H.: Counterexamples Revisited: Principles, Algorithms, Applications. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 208\u2013224. Springer, Heidelberg (2004)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","year":"2007","unstructured":"Damm, W., Hermanns, H. (eds.): CAV 2007. LNCS, vol.\u00a04590. Springer, Heidelberg (2007)"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Groce, A.: Error Explanation and Fault Localization with Distance Metrics. PhD thesis, Carnegie Mellon University (2005)","DOI":"10.1007\/s10009-005-0202-0"},{"key":"9_CR13","unstructured":"Lynce, I., Marques Silva, J.: On computing minimum unsatisfiable cores. In: SAT (2004)"},{"key":"9_CR14","first-page":"821","volume-title":"DAC","author":"I. Pill","year":"2006","unstructured":"Pill, I., et al.: Formal analysis of hardware requirements. In: Sentovich, E. (ed.) DAC, pp. 821\u2013826. ACM Press, New York (2006)"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","first-page":"364","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Pnueli","year":"2005","unstructured":"Pnueli, A., Piterman, N., Sa\u2019ar, Y.: Synthesis of Reactive(1) Designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 364\u2013380. Springer, Heidelberg (2005)"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: 16th Annual ACM Symposium on Principles of Programming Languages, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"9_CR17","first-page":"319","volume-title":"FOCS","author":"S. Safra","year":"1988","unstructured":"Safra, S.: On the complexity of omega-automata. In: FOCS, pp. 319\u2013327. IEEE, Los Alamitos (1988)"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48119-2_15","volume-title":"FM\u201999 - Formal Methods","author":"S. Tripakis","year":"1999","unstructured":"Tripakis, S., Altisen, K.: On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, Springer, Heidelberg (1999)"},{"key":"9_CR19","unstructured":"http:\/\/www.prosyd.org"},{"key":"9_CR20","first-page":"34","volume-title":"SEFM","author":"N. Yoshiura","year":"2004","unstructured":"Yoshiura, N.: Finding the causes of unrealizability of reactive system formal specifications. In: SEFM, pp. 34\u201343. IEEE Computer Society Press, Los Alamitos (2004)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78163-9_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:00:39Z","timestamp":1619521239000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78163-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540781622","9783540781639"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78163-9_9","relation":{},"subject":[]}}