{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T04:15:39Z","timestamp":1769746539358,"version":"3.49.0"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[2011,12,16]],"date-time":"2011-12-16T00:00:00Z","timestamp":1323993600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2013,10]]},"DOI":"10.1007\/s10009-011-0221-y","type":"journal-article","created":{"date-parts":[[2011,12,15]],"date-time":"2011-12-15T19:47:18Z","timestamp":1323978438000},"page":"563-583","source":"Crossref","is-referenced-by-count":41,"title":["Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies"],"prefix":"10.1007","volume":"15","author":[{"given":"Robert","family":"K\u00f6nighofer","sequence":"first","affiliation":[]},{"given":"Georg","family":"Hofferek","sequence":"additional","affiliation":[]},{"given":"Roderick","family":"Bloem","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,12,16]]},"reference":[{"key":"221_CR1","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: time for playing games! In: Proceedings of Computer Aided Verification (CAV\u201907), pp. 121\u2013125 (2007)","DOI":"10.1007\/978-3-540-73368-3_14"},{"key":"221_CR2","doi-asserted-by":"crossref","unstructured":"Bloem, R., Cimatti, A., Greimel, K., Hofferek, G., Koenighofer, R., Roveri, M., Schuppan, V., Seeber, R.: RATSY\u2014a new requirements analysis tool with synthesis. In: Proceedings of Computer Aided Verification. LNCS, vol. 6174, pp. 425\u2013429 (2010)","DOI":"10.1007\/978-3-642-14295-6_37"},{"key":"221_CR3","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Automatic hardware synthesis from specifications: a case study. In: Proceedings of the Design, Automation and Test in Europe, pp. 1188\u20131193 (2007)","DOI":"10.1109\/DATE.2007.364456"},{"key":"221_CR4","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: Hardware form PSL. In: 6th International Workshop on Compiler Optimization Meets Compiler Verification. Electronic Notes in Theoretical Computer Science (2007)","DOI":"10.1016\/j.entcs.2007.09.004"},{"issue":"2","key":"221_CR5","first-page":"139","volume":"62","author":"Y. Bontemps","year":"2004","unstructured":"Bontemps Y., Schobbens P.-Y., L\u00f6ding C.: Synthesis of open reactive systems from scenario-based specifications. Fundamamenta Informaticae 62(2), 139\u2013169 (2004)","journal-title":"Fundamamenta Informaticae"},{"issue":"8","key":"221_CR6","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comput. C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"221_CR7","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T., Jobstmann, B.: Environment assumptions for synthesis. In: International Conference on Concurrency Theory (CONCUR), pp. 147\u2013161 (2008)","DOI":"10.1007\/978-3-540-85361-9_14"},{"key":"221_CR8","doi-asserted-by":"crossref","unstructured":"Chockler, H., Kupferman, O., Kurshan, R.P., Vardi, M. Y.: A practical approach to coverage in model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) Thirteenth Conference on Computer Aided Verification (CAV\u201901). LNCS, vol. 2102, pp. 66\u201378. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44585-4_7"},{"key":"221_CR9","doi-asserted-by":"crossref","unstructured":"Chockler, H., Kupferman, O., Vardi, M.Y.: Coverage metrics for temporal logic model checking. In: Tools and algorithms for the construction and analysis of systems (TACAS). LNCS, vol. 2031, pp. 528\u2013542. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45319-9_36"},{"key":"221_CR10","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In: Proceedings of the International Conference on Computer-Aided Verification (CAV\u201902) (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"221_CR11","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Roveri, M., Schuppan, V., Tchaltsev, A.: Diagnostic information for realizability. In: Proceedings of Verification, Model Checking, and Abstract Interpretation (VMCAI\u201908), pp. 52\u201367 (2008)","DOI":"10.1007\/978-3-540-78163-9_9"},{"key":"221_CR12","doi-asserted-by":"crossref","unstructured":"Claessen, K.: A coverage analysis for safety property lists. In: Proceedings of Formal Methods in Computer Aided Design, pp. 139\u2013145 (2007)","DOI":"10.1109\/FMCAD.2007.4401992"},{"key":"221_CR13","doi-asserted-by":"crossref","unstructured":"Console, L., Friedrich, G., Dupr\u00e9, D. Theseider: Model-based diagnosis meets error diagnosis in logic programs. In: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI\u201993), pp. 1494\u20131499. Morgan-Kaufmann, Menlo Park (1993)","DOI":"10.1007\/BFb0019402"},{"key":"221_CR14","unstructured":"Das, S., Banerjee, A., Basu, P., Dasgupta, P., Chakrabarti, P.P., Mohan, C.R., Fix, L.: Formal methods for analyzing the completeness of an assertion suite against a high-level fault model. In: VLSI Design, pp. 201\u2013206 (2005)"},{"key":"221_CR15","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0004-3702(87)90063-4","volume":"32","author":"J. de Kleer","year":"1987","unstructured":"de Kleer J., Williams B.C.: Diagnosing multiple faults. Artif. Intell. 32, 97\u2013130 (1987)","journal-title":"Artif. Intell."},{"key":"221_CR16","unstructured":"Dellacherie, S.: Automatic bus-protocol verification using assertions. In: Global Signal Processing Expo Conference (GSPx) (2004)"},{"key":"221_CR17","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1016\/S0004-3702(03)00117-6","volume":"152","author":"A. Felfernig","year":"2004","unstructured":"Felfernig A., Friedrich G., Jannach D., Stumptner M.: Consistency-based diagnosis of configuration knowledge bases. Artif. Intell. 152, 213\u2013234 (2004)","journal-title":"Artif. Intell."},{"key":"221_CR18","doi-asserted-by":"crossref","unstructured":"Filiot, E., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: Proceedings of Computer Aided Verification, pp. 263\u2013277 (2009)","DOI":"10.1007\/978-3-642-02658-4_22"},{"key":"221_CR19","doi-asserted-by":"crossref","unstructured":"Fisman, D., Kupferman, O., Seinvald, S., Vardi, M.Y.: A framework for inverent vacuity. In: Proceedings of Haifa Verification Conference (HVC) (2008)","DOI":"10.1007\/978-3-642-01702-5_7"},{"key":"221_CR20","doi-asserted-by":"crossref","unstructured":"Friedrich, G., Shchekotykhin, K.M.: A general diagnosis method for ontologies. In: International Semantic Web Conference, pp. 232\u2013246 (2005)","DOI":"10.1007\/11574620_19"},{"issue":"1-2","key":"221_CR21","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0004-3702(99)00034-X","volume":"111","author":"G. Friedrich","year":"1999","unstructured":"Friedrich G., Stumptner M., Wotawa F.: Model-based diagnosis of hardware designs. Artif. Intell. 111(1-2), 3\u201339 (1999)","journal-title":"Artif. Intell."},{"key":"221_CR22","doi-asserted-by":"crossref","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds): Automata, Logics, and Infinite Games: A Guide to Current Research. LNCS, vol. 2500. Springer (2002)","DOI":"10.1007\/3-540-36387-4"},{"key":"221_CR23","doi-asserted-by":"crossref","unstructured":"Gro\u00dfe, D., K\u00fchne, U., Drechsler, R.: Estimating functional coverage in bounded model checking. In: Proceedings of the Conference on Design Automation and Test in Europe (DATE\u201907), pp. 1176\u20131181 (2007)","DOI":"10.1109\/DATE.2007.364454"},{"key":"221_CR24","doi-asserted-by":"crossref","unstructured":"Hoskote, Y., Kam, T., Ho, P.-H., Zhao, X.: Coverage estimation for symbolic model checking. In: Proceedings of Design Automation Conference, pp. 300\u2013305 (1999)","DOI":"10.1145\/309847.309936"},{"key":"221_CR25","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: 6th Conference on Formal Methods in Computer Aided Design (FMCAD\u201906), pp. 117\u2013124 (2006)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"221_CR26","doi-asserted-by":"crossref","unstructured":"Katz, S., Grumberg, O., Geist, D.: \u201cHave I written enough properties?\u201d\u2014A method of comparison between specification and implementation. In: Correct Hardware Design and Verification Methods (CHARME\u201999). LNCS, vol. 1703, pp. 280\u2013297. Springer (1999)","DOI":"10.1007\/3-540-48153-2_21"},{"key":"221_CR27","doi-asserted-by":"crossref","unstructured":"Koenighofer, R., Hofferek, G., Bloem, R.: Debugging formal specifications using simple counterstrategies. In: Proceedings of Formal Methods in Computer Aided Design (FMCAD\u201909), pp. 152\u2013159 (2009)","DOI":"10.1109\/FMCAD.2009.5351127"},{"key":"221_CR28","doi-asserted-by":"crossref","unstructured":"Koenighofer, R., Hofferek, G., Bloem, R.: Debugging unrealizable specifications with model-based diagnosis. In: Proceedings of Haifa Verification Conference (HVC). LNCS, vol. 6504, pp. 29\u201345. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-19583-9_8"},{"key":"221_CR29","unstructured":"K\u00f6nighofer, R.: Debugging formal specifications with simplified counterstrategies. Master\u2019s thesis, IAIK, Graz University of Technology, Inffeldgasse 16a, A-8010 Graz, Austria, (2009)"},{"key":"221_CR30","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen D.: Results on the propositional\u00a0\u03bc-calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"221_CR31","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Foundations of Computer Science, pp. 531\u2013542 (2005)","DOI":"10.1109\/SFCS.2005.66"},{"key":"221_CR32","doi-asserted-by":"crossref","unstructured":"Leucker, M.: Model checking games for the alternation-free\u00a0\u03bc-calculus and alternating automata. In: Proceedings of the International Conference on Logic Programming and Automated Reasoning (LPAR\u201999), pp. 77\u201391. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48242-3_6"},{"key":"221_CR33","doi-asserted-by":"crossref","unstructured":"Leucker, M., Noll, T.: Truth\/SLC\u2014a parallel verification platform for concurrent systems. In: Computer Aided Verification, pp. 255\u2013259. Springer, Berlin (2001)","DOI":"10.1007\/3-540-44585-4_24"},{"issue":"1","key":"221_CR34","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"M.H. Liffiton","year":"2008","unstructured":"Liffiton M.H., Sakallah K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. 40(1), 1\u201333 (2008)","journal-title":"J. Autom. Reason."},{"key":"221_CR35","unstructured":"Mateis, C., Stumptner, M., Wieland, D., Wotawa, F.: Model-based debugging of java programs. In: AADEBUG (2000)"},{"key":"221_CR36","doi-asserted-by":"crossref","unstructured":"Morgenstern, A., Schneider, K.: Exploiting the temporal logic hierarchy and the non-confluence property for efficient LTL synthesis. CoRR, abs\/1006.1408 (2010)","DOI":"10.4204\/EPTCS.25.11"},{"key":"221_CR37","unstructured":"Mori, R., Yonezaki, N.: Several realizability concepts in reactive objects. In: Information Modeling and Knowledge Bases (1993)"},{"key":"221_CR38","doi-asserted-by":"crossref","unstructured":"Pill, I., Semprini, S., Cavada, R., Roveri, M., Bloem, R., Cimatti, A.: Formal analysis of hardware requirements. In: Design Automation Conference, pp. 821\u2013826 (2006)","DOI":"10.1109\/DAC.2006.229231"},{"key":"221_CR39","doi-asserted-by":"crossref","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: 7th International Conference on Verification, Model Checking and Abstract Interpretation. LNCS, vol. 3855, pp. 364\u2013380. Springer, Berlin (2006)","DOI":"10.1007\/11609773_24"},{"key":"221_CR40","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings Symposium on Principles of Programming Languages (POPL \u201989), pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"221_CR41","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0004-3702(87)90062-2","volume":"32","author":"R. Reiter","year":"1987","unstructured":"Reiter R.: A theory of diagnosis from first principles. Artif. Intell. 32, 57\u201395 (1987)","journal-title":"Artif. Intell."},{"key":"221_CR42","unstructured":"Rosner, R.: Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science (1992)"},{"key":"221_CR43","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package. University of Colorado at Boulder, ftp:\/\/vlsi.colorado.edu\/pub\/"},{"key":"221_CR44","doi-asserted-by":"crossref","unstructured":"Stevens, P., Stirling, C.: Practical model-checking using games. In: Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 1384. Springer, Berlin (1998)","DOI":"10.1007\/BFb0054166"},{"key":"221_CR45","doi-asserted-by":"crossref","unstructured":"Stirling, C.: Local model checking games. In: Proceedings of Concurrency Theory, pp. 1\u201311. Springer, Berlin (1995)","DOI":"10.1007\/3-540-60218-6_1"},{"key":"221_CR46","unstructured":"Stumptner, M., Wotawa, F.: Debugging functional programs. In: Proceedings on the 16th International Joint Conference on Artificial Intelligence (1999)"},{"key":"221_CR47","doi-asserted-by":"crossref","unstructured":"Tan, L.: PlayGame: A platform for diagnostic games. In: Computer Aided Verification. LNCS, vol. 3114, pp. 492\u2013495. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-27813-9_44"},{"key":"221_CR48","doi-asserted-by":"crossref","unstructured":"Tripakis, S., Altisen, K.: On-the-fly controller synthesis for discrete and dense-time systems. In: World Congress on Formal Methods, pp. 233\u2013252 (1999)","DOI":"10.1007\/3-540-48119-2_15"},{"key":"221_CR49","doi-asserted-by":"crossref","unstructured":"Yoshiura, N.: Finding the causes of unrealizability of reactive system formal specifications. In: Proceedings of Software Engineering and Formal Methods (SEFM\u201904), pp. 34\u201343 (2004)","DOI":"10.1109\/SEFM.2004.1347501"},{"issue":"2","key":"221_CR50","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1109\/32.988498","volume":"28","author":"A. Zeller","year":"2002","unstructured":"Zeller A., Hildebrandt R.: Simplifying and isolating failure-inducing input. IEEE Trans. Softw. Eng. 28(2), 183\u2013200 (2002)","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0221-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-011-0221-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0221-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,15]],"date-time":"2025-03-15T22:42:12Z","timestamp":1742078532000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-011-0221-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,12,16]]},"references-count":50,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2013,10]]}},"alternative-id":["221"],"URL":"https:\/\/doi.org\/10.1007\/s10009-011-0221-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,12,16]]}}}