{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,18]],"date-time":"2026-01-18T03:38:04Z","timestamp":1768707484506,"version":"3.49.0"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319234038","type":"print"},{"value":"9783319234045","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-23404-5_6","type":"book-chapter","created":{"date-parts":[[2015,8,26]],"date-time":"2015-08-26T00:57:19Z","timestamp":1440550639000},"page":"66-83","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["On Refinement of B\u00fcchi Automata for Explicit Model Checking"],"prefix":"10.1007","author":[{"given":"Franti\u0161ek","family":"Blahoudek","sequence":"first","affiliation":[]},{"given":"Alexandre","family":"Duret-Lutz","sequence":"additional","affiliation":[]},{"given":"Vojt\u011bch","family":"Rujbr","sequence":"additional","affiliation":[]},{"given":"Jan","family":"Strej\u010dek","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,8,27]]},"reference":[{"key":"6_CR1","unstructured":"Accellera. Property specification language reference manual v1.1 (2004). http:\/\/www.eda.org\/vfv\/"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-642-28756-5_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Babiak","year":"2012","unstructured":"Babiak, T., K\u0159et\u00ednsk\u00fd, M., \u0158eh\u00e1k, V., Strej\u010dek, J.: LTL to b\u00fcchi automata translation: fast and more deterministic. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 95\u2013109. Springer, Heidelberg (2012)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-642-39176-7_6","volume-title":"Model Checking Software","author":"T Babiak","year":"2013","unstructured":"Babiak, T., Badie, T., Duret-Lutz, A., K\u0159et\u00ednsk\u00fd, M., Strej\u010dek, J.: Compositional approach to suspension and other improvements to LTL translation. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 81\u201398. Springer, Heidelberg (2013)"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Blahoudek, F., Duret-Lutz, A., K\u0159et\u00ednsk\u00fd, M., Strej\u010dek, J.: Is there a best B\u00fcchi automaton for explicit model checking? In: SPIN 2014, pp. 68\u201376. ACM (2014)","DOI":"10.1145\/2632362.2632377"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-75596-8_17","volume-title":"Automated Technology for Verification and Analysis","author":"C Dax","year":"2007","unstructured":"Dax, C., Eisinger, J., Klaedtke, F.: Mechanizing the powerset construction for restricted classes of $$\\omega $$-automata. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 223\u2013236. Springer, Heidelberg (2007)"},{"issue":"1\/2","key":"6_CR6","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1504\/IJCCBS.2014.059594","volume":"5","author":"A Duret-Lutz","year":"2014","unstructured":"Duret-Lutz, A.: LTL translation improvements in Spot 1.0. Int. J. Crit. Comput. Based Syst. 5(1\/2), 31\u201354 (2014)","journal-title":"Int. J. Crit. Comput. Based Syst."},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45139-0_5","volume-title":"Model Checking Software","author":"S Edelkamp","year":"2001","unstructured":"Edelkamp, S., Lluch Lafuente, A., Leue, S.: Directed explicit model checking with HSF-SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, p. 57. Springer, Heidelberg (2001)"},{"issue":"2\u20133","key":"6_CR8","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s10009-002-0104-3","volume":"5","author":"S Edelkamp","year":"2004","unstructured":"Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. STTT 5(2\u20133), 247\u2013267 (2004)","journal-title":"STTT"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/3-540-44618-4_13","volume-title":"CONCUR 2000 - Concurrency Theory","author":"K Etessami","year":"2000","unstructured":"Etessami, K., Holzmann, G.J.: Optimizing b\u00fcchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 153\u2013167. Springer, Heidelberg (2000)"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to b\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"6_CR11","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Boston (2003)"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Peled, D.A., Yannakakis, M.: On nested depth first search. In: SPIN 1996, vol. 32 of DIMACS. American Mathematical Society (1996)","DOI":"10.1090\/dimacs\/032\/03"},{"key":"6_CR13","unstructured":"Minato, S.: Fast generation of irredundant sum-of-products forms from binary decision diagrams. In: SASIMI 1992, pp. 64\u201373 (1992)"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-73370-6_17","volume-title":"Model Checking Software","author":"R Pel\u00e1nek","year":"2007","unstructured":"Pel\u00e1nek, R.: BEEM: benchmarks for explicit model checkers. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263\u2013267. Springer, Heidelberg (2007)"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-540-39724-3_12","volume-title":"Correct Hardware Design and Verification Methods","author":"R Sebastiani","year":"2003","unstructured":"Sebastiani, R., Tonetta, S.: \u201cMore Deterministic\u201d vs. \u201cSmaller\u201d b\u00fcchi automata for efficient LTL model checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 126\u2013140. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23404-5_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T15:43:26Z","timestamp":1676475806000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-23404-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319234038","9783319234045"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23404-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"27 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}