{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T02:54:10Z","timestamp":1742957650872,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319675480"},{"type":"electronic","value":"9783319675497"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-67549-7_14","type":"book-chapter","created":{"date-parts":[[2017,9,14]],"date-time":"2017-09-14T12:56:18Z","timestamp":1505393778000},"page":"230-242","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Homing Sequence Derivation with Quantified Boolean Satisfiability"],"prefix":"10.1007","author":[{"given":"Hung-En","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kuan-Hua","family":"Tu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jie-Hong R.","family":"Jiang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Natalia","family":"Kushik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,15]]},"reference":[{"issue":"1","key":"14_CR1","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/s10703-012-0152-6","volume":"41","author":"V Balabanov","year":"2012","unstructured":"Balabanov, V., Jiang, J.H.R.: Unified QBF certification and its applications. Formal Methods Syst. Des. 41(1), 45\u201365 (2012)","journal-title":"Formal Methods Syst. Des."},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-319-40970-2_28","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"V Balabanov","year":"2016","unstructured":"Balabanov, V., Jiang, J.-H.R., Scholl, C., Mishchenko, A., Brayton, R.K.: 2QBF: challenges and solutions. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 453\u2013469. Springer, Cham (2016). doi:10.1007\/978-3-319-40970-2_28"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24\u201340. Springer, Heidelberg (2010). doi:10.1007\/978-3-642-14295-6_5"},{"issue":"3","key":"14_CR4","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1109\/TSE.1978.231496","volume":"4","author":"TS Chow","year":"1978","unstructured":"Chow, T.S.: Testing software design modeled by finite-state machines. IEEE Trans. Softw. Eng. 4(3), 178\u2013187 (1978)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Haddad, A.R.: Efficient Algorithms for Constructing Preset Distinguishing Sequences for Nondeterministic Finite State Machines. Master\u2019s thesis, American University of Sharjah (2016)","DOI":"10.1109\/ICMSAO.2017.7934857"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-642-31612-8_10","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"M Janota","year":"2012","unstructured":"Janota, M., Klieber, W., Marques-Silva, J., Clarke, E.: Solving QBF with counterexample guided refinement. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 114\u2013128. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-31612-8_10"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Jiang, J.H.R., Devadas, S.: Logic synthesis in a nutshell. In: Wang, L.T., Chang, Y.W., Cheng, K.T. (eds.) Electronic Design Automation: Synthesis, Verification, and Test. Elsevier (2009)","DOI":"10.1016\/B978-0-12-374364-0.50013-8"},{"key":"14_CR8","volume-title":"Switching and Finite Automata Theory","author":"Z Kohavi","year":"1978","unstructured":"Kohavi, Z.: Switching and Finite Automata Theory. McGraw-Hill, New York (1978)"},{"issue":"6","key":"14_CR9","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1134\/S0361768814060140","volume":"40","author":"NG Kushik","year":"2014","unstructured":"Kushik, N.G., Kulyamin, V.V., Evtushenko, N.V.: On the complexity of existence of homing sequences for nondeterministic finite state machines. Program. Comput. Softw. 40(6), 333\u2013336 (2014)","journal-title":"Program. Comput. Softw."},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-642-39274-0_20","volume-title":"Implementation and Application of Automata","author":"N Kushik","year":"2013","unstructured":"Kushik, N., Yevtushenko, N.: On the length of homing sequences for nondeterministic finite state machines. In: Konstantinidis, S. (ed.) CIAA 2013. LNCS, vol. 7982, pp. 220\u2013231. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-39274-0_20"},{"issue":"8","key":"14_CR11","doi-asserted-by":"publisher","first-page":"1090","DOI":"10.1109\/5.533956","volume":"84","author":"D Lee","year":"1996","unstructured":"Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines - a survey. Proc. IEEE 84(8), 1090\u20131123 (1996)","journal-title":"Proc. IEEE"},{"issue":"2\u20133","key":"14_CR12","doi-asserted-by":"crossref","first-page":"71","DOI":"10.3233\/SAT190077","volume":"7","author":"F Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: DepQBF: a dependency-aware QBF solver. J. Satisfiability, Boolean Model. Comput. 7(2\u20133), 71\u201376 (2010)","journal-title":"J. Satisfiability, Boolean Model. Comput."},{"key":"14_CR13","unstructured":"Mishchenko, A., Chatterjee, S., Jiang, J.H.R., Brayton, R.K.: FRAIGs: a unifying representation for logic synthesis and verification. In: ERL Technical report. UC Berkeley (2005)"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/11498490_2","volume-title":"Model-Based Testing of Reactive Systems","author":"S Sandberg","year":"2005","unstructured":"Sandberg, S.: 1 homing and synchronizing sequences. In: Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.) Model-Based Testing of Reactive Systems. LNCS, vol. 3472, pp. 5\u201333. Springer, Heidelberg (2005). doi:10.1007\/11498490_2"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Shabaldina, N., Gromov, M.: FSMTest-1.0: a manual for researches. In: EWDTS. pp. 1\u20134 (2015)","DOI":"10.1109\/EWDTS.2015.7493141"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logic, pp. 466\u2013483 (1970)","DOI":"10.1007\/978-3-642-81955-1_28"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-24318-4_25","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"K-H Tu","year":"2015","unstructured":"Tu, K.-H., Hsu, T.-C., Jiang, J.-H.R.: QELL: QBF reasoning with extended clause learning and levelized SAT solving. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 343\u2013359. Springer, Cham (2015). doi:10.1007\/978-3-319-24318-4_25"},{"key":"14_CR18","first-page":"98","volume":"4","author":"M Vasilevskii","year":"1973","unstructured":"Vasilevskii, M.: Failure diagnosis of automata. Kibernetika 4, 98\u2013108 (1973)","journal-title":"Kibernetika"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Yenig\u00fcn, H., Yevtushenko, N., Kushik, N.: Some classes of finite state machines with polynomial length of distinguishing test cases. In: SAC, pp. 1680\u20131685 (2016)","DOI":"10.1145\/2851613.2851835"}],"container-title":["Lecture Notes in Computer Science","Testing Software and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67549-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,25]],"date-time":"2021-09-25T02:36:47Z","timestamp":1632537407000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-67549-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319675480","9783319675497"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67549-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"15 September 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTSS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"IFIP International Conference on Testing Software and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"St. Petersburg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Russia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 October 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"pts2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.ictss2017.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}