{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T00:00:33Z","timestamp":1742947233771,"version":"3.40.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319948201"},{"type":"electronic","value":"9783319948218"}],"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-94821-8_18","type":"book-chapter","created":{"date-parts":[[2018,7,3]],"date-time":"2018-07-03T13:25:55Z","timestamp":1530624355000},"page":"306-323","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verifying the LTL to B\u00fcchi Automata Translation via Very Weak Alternating Automata"],"prefix":"10.1007","author":[{"given":"Simon","family":"Jantsch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Norrish","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,4]]},"reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-40648-0_23","volume-title":"NASA Formal Methods","author":"J Brunner","year":"2016","unstructured":"Brunner, J., Lammich, P.: Formal verification of an executable LTL model checker with partial order reduction. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 307\u2013321. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40648-0_23"},{"issue":"2","key":"18_CR2","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. Form. Meth. Syst. Des. 1(2), 275\u2013288 (1992)","journal-title":"Form. Meth. Syst. Des."},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/11537328_15","volume-title":"Model Checking Software","author":"J-M Couvreur","year":"2005","unstructured":"Couvreur, J.-M., Duret-Lutz, A., Poitrenaud, D.: On-the-fly emptiness checks for generalized B\u00fcchi automata. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 169\u2013184. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11537328_15"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Erwig, M.: Functional programming with graphs. In: Simon, L., Jones, P., Tofte, M., Berman, A.M. (eds.) Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP 1997), Amsterdam, The Netherlands, 9\u201311 June 1997, pp. 52\u201365. ACM (1997)","DOI":"10.1145\/258949.258955"},{"issue":"3","key":"18_CR5","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10703-016-0259-2","volume":"49","author":"J Esparza","year":"2016","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J., Sickert, S.: From LTL to deterministic automata - a safraless compositional approach. Form. Meth. Syst. Des. 49(3), 219\u2013271 (2016)","journal-title":"Form. Meth. Syst. Des."},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-39799-8_31","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2013","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.-G.: A fully verified executable LTL model checker. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 463\u2013478. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_31"},{"key":"18_CR7","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). https:\/\/doi.org\/10.1007\/3-540-44585-4_6"},{"key":"18_CR8","doi-asserted-by":"publisher","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembi\u0144ski, P., \u015aredniawa, M. (eds.) Protocol Specification, Testing and Verification XV, PSTV 1995. IFIP Advances in Information and Communication Technology, pp. 3\u201318. Springer, Boston (1996). https:\/\/doi.org\/10.1007\/978-0-387-34892-6_1","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-39634-2_9","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2013","unstructured":"Lammich, P.: Automatic data refinement. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 84\u201399. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_9"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-32347-8_12","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2012","unstructured":"Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft\u2019s algorithm. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 166\u2013182. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_12"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/3-540-44929-9_36","volume-title":"Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics","author":"C Loding","year":"2000","unstructured":"Loding, C., Thomas, W.: Alternating automata and logics over infinite words. In: van Leeuwen, J., Watanabe, O., Hagiya, M., Mosses, P.D., Ito, T. (eds.) TCS 2000. LNCS, vol. 1872, pp. 521\u2013535. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44929-9_36"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/3-540-44659-1_26","volume-title":"Theorem Proving in Higher Order Logics","author":"S Merz","year":"2000","unstructured":"Merz, S.: Weak alternating automata in Isabelle\/HOL. In: Aagaard, M., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 424\u2013441. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44659-1_26"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Myreen, M.O., Owens, S.: Proof-producing synthesis of ML from higher-order logic. In: Thiemann, P., Findler, R.B. (eds.) ACM SIGPLAN International Conference on Functional Programming, ICFP 2012, Copenhagen, Denmark, 9\u201315 September 2012, pp. 115\u2013126. ACM (2012)","DOI":"10.1145\/2398856.2364545"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-319-12154-3_7","volume-title":"Verified Software: Theories, Tools and Experiments","author":"R Neumann","year":"2014","unstructured":"Neumann, R.: Using promela in a fully verified executable LTL model checker. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 105\u2013114. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12154-3_7"},{"key":"18_CR15","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-642-03359-9","volume-title":"Theorem Proving in Higher Order Logics: Proceedings of 22nd International Conference, TPHOLs 2009, Munich, Germany, 17\u201320 August 2009","author":"A Schimpf","year":"2009","unstructured":"Schimpf, A., Merz, S., Smaus, J.-G.: Construction of B\u00fcchi automata for LTL model checking verified in Isabelle\/HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics: Proceedings of 22nd International Conference, TPHOLs 2009, Munich, Germany, 17\u201320 August 2009, pp. 424\u2013439. Berlin, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-662-45824-2_11","volume-title":"Logic and Its Applications","author":"A Schimpf","year":"2015","unstructured":"Schimpf, A., Smaus, J.-G.: B\u00fcchi automata optimisations formalised in Isabelle\/HOL. In: Banerjee, M., Krishna, S.N. (eds.) ICLA 2015. LNCS, vol. 8923, pp. 158\u2013169. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-45824-2_11"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/3-540-57887-0_116","volume-title":"Theoretical Aspects of Computer Software","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y.: Nontraditional applications of automata theory. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 575\u2013597. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-57887-0_116"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/3-540-63104-6_19","volume-title":"Automated Deduction\u2014CADE-14","author":"MY Vardi","year":"1997","unstructured":"Vardi, M.Y.: Alternating automata: unifying truth and validity checking for temporal logics. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 191\u2013206. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63104-6_19"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94821-8_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T05:02:18Z","timestamp":1571547738000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94821-8_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319948201","9783319948218"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94821-8_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"ITP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Interactive Theorem Proving","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oxford","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"itp2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/itp2018.inria.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}