{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T09:17:40Z","timestamp":1743153460889,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031067723"},{"type":"electronic","value":"9783031067730"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[[2022]]},"DOI":"10.1007\/978-3-031-06773-0_30","type":"book-chapter","created":{"date-parts":[[2022,5,19]],"date-time":"2022-05-19T11:24:44Z","timestamp":1652959484000},"page":"557-575","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["On-the-Fly Model Checking with\u00a0Neural MCTS"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4973-8458","authenticated-orcid":false,"given":"Ruiyang","family":"Xu","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1158-0413","authenticated-orcid":false,"given":"Karl","family":"Lieberherr","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,5,20]]},"reference":[{"key":"30_CR1","unstructured":"Anthony, T., Tian, Z., Barber, D.: Thinking fast and slow with deep learning and tree search. In: Proceedings of the 31st International Conference on Neural Information Processing Systems. NIPS 2017, pp. 5366\u20135376 (2017)"},{"key":"30_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-540-74128-2_6","volume-title":"Model Checking and Artificial Intelligence","author":"T Araragi","year":"2007","unstructured":"Araragi, T., Cho, S.M.: Checking liveness properties of concurrent systems by reinforcement learning. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt 2006. LNCS (LNAI), vol. 4428, pp. 84\u201394. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74128-2_6"},{"issue":"2","key":"30_CR3","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1023\/A:1013689704352","volume":"47","author":"P Auer","year":"2002","unstructured":"Auer, P., Cesa-Bianchi, N., Fischer, P.: Finite-time analysis of the multiarmed bandit problem. Mach. Learn. 47(2), 235\u2013256 (2002)","journal-title":"Mach. Learn."},{"key":"30_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-642-40988-2_13","volume-title":"Machine Learning and Knowledge Discovery in Databases","author":"D Auger","year":"2013","unstructured":"Auger, D., Cou\u00ebtoux, A., Teytaud, O.: Continuous upper confidence trees with polynomial exploration \u2013 consistency. In: Blockeel, H., Kersting, K., Nijssen, S., \u017delezn\u00fd, F. (eds.) ECML PKDD 2013. LNCS (LNAI), vol. 8188, pp. 194\u2013209. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40988-2_13"},{"key":"30_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-642-11623-0_17","volume-title":"Fundamentals of Software Engineering","author":"R Behjati","year":"2010","unstructured":"Behjati, R., Sirjani, M., Nili Ahmadabadi, M.: Bounded rational search for on-the-fly model checking of LTL properties. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS, vol. 5961, pp. 292\u2013307. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11623-0_17"},{"issue":"1","key":"30_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/TCIAIG.2012.2186810","volume":"4","author":"C Browne","year":"2012","unstructured":"Browne, C., et al.: A survey of monte Carlo tree search methods. IEEE Trans. Comput. Intellig. AI Games 4(1), 1\u201343 (2012)","journal-title":"IEEE Trans. Comput. Intellig. AI Games"},{"key":"30_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35746-6_1","volume-title":"Tools for Practical Software Verification","author":"EM Clarke","year":"2012","unstructured":"Clarke, E.M., Klieber, W., Nov\u00e1\u010dek, M., Zuliani, P.: Model checking and the state explosion problem. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 1\u201330. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35746-6_1"},{"issue":"4","key":"30_CR8","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"EM Clarke","year":"1996","unstructured":"Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv. 28(4), 626\u2013643 (1996)","journal-title":"ACM Comput. Surv."},{"key":"30_CR9","unstructured":"Grill, J.B., et al.: Monte-Carlo Tree Search as Regularized Policy Optimization. arXiv:abs\/2007.12509 (2020)"},{"key":"30_CR10","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/BFb0099486","volume-title":"Computation and Proof Theory","author":"Y Gurevich","year":"1984","unstructured":"Gurevich, Y.: Toward logic tailored for computational complexity. In: B\u00f6rger, E., Oberschelp, W., Richter, M.M., Schinzel, B., Thomas, W. (eds.) Computation and Proof Theory. LNM, vol. 1104, pp. 175\u2013216. Springer, Heidelberg (1984). https:\/\/doi.org\/10.1007\/BFb0099486"},{"key":"30_CR11","doi-asserted-by":"crossref","unstructured":"Gurevich, Y., Shelah, S.: Fixed-point extensions of first-order logic. In: 26th Annual Symposium on Foundations of Computer Science (SFCS 1985), pp. 346\u2013353 (1985)","DOI":"10.1109\/SFCS.1985.27"},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"Hella, L., Kuusisto, A., R\u00f6nnholm, R.: Bounded game-theoretic semantics for modal mu-calculus and some variants. In: Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, Belgium, September 21\u201322, 2020. EPTCS, vol. 326, pp. 82\u201396 (2020)","DOI":"10.4204\/EPTCS.326.6"},{"issue":"2","key":"30_CR13","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1305\/ndjfl\/1093883627","volume":"23","author":"J Hintikka","year":"1982","unstructured":"Hintikka, J.: Game-theoretical semantics: insights and prospects. Notre Dame J. Formal Logic 23(2), 219\u2013241 (1982)","journal-title":"Notre Dame J. Formal Logic"},{"issue":"5","key":"30_CR14","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G Holzmann","year":"1997","unstructured":"Holzmann, G.: The model checker SPIN. IEEE Trans. Software Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Software Eng."},{"key":"30_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/3-540-61604-7_60","volume-title":"CONCUR \u201996: Concurrency Theory","author":"D Janin","year":"1996","unstructured":"Janin, D., Walukiewicz, I.: On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 263\u2013277. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61604-7_60"},{"key":"30_CR16","unstructured":"Kadam, P., Xu, R., Lieberherr, K.J.: Dual Monte Carlo Tree Search. CoRR abs\/2103.11517 (2021)"},{"key":"30_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/11871842_29","volume-title":"Machine Learning: ECML 2006","author":"L Kocsis","year":"2006","unstructured":"Kocsis, L., Szepesv\u00e1ri, C.: Bandit based monte-Carlo planning. In: F\u00fcrnkranz, J., Scheffer, T., Spiliopoulou, M. (eds.) ECML 2006. LNCS (LNAI), vol. 4212, pp. 282\u2013293. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11871842_29"},{"key":"30_CR18","doi-asserted-by":"publisher","unstructured":"Kolaitis, P.G.: On the expressive power of logics on finite models. In: Finite Model Theory and Its Applications. Texts in Theoretical Computer Science an EATCS Series, pp. 27\u2013123. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/3-540-68804-8_2","DOI":"10.1007\/3-540-68804-8_2"},{"key":"30_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/3-540-46002-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 52\u201366. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_5"},{"issue":"1&2","key":"30_CR20","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/0304-3975(95)00136-0","volume":"163","author":"D Niwinski","year":"1996","unstructured":"Niwinski, D., Walukiewicz, I.: Games for the mu-Calculus. Theor. Comput. Sci. 163(1&2), 99\u2013116 (1996)","journal-title":"Theor. Comput. Sci."},{"key":"30_CR21","doi-asserted-by":"publisher","unstructured":"Rebuschi, M.: Extended game-theoretical semantics. In: Trobok, M., Mi\u0161\u010devi\u0107, N., \u017darni\u0107, B. (eds.) Between Logic and Reality. Logic, Epistemology, and the Unity of Science, vol. 25, pp. 161\u2013182. Springer, Dordrecht (2012). https:\/\/doi.org\/10.1007\/978-94-007-2390-0_9","DOI":"10.1007\/978-94-007-2390-0_9"},{"key":"30_CR22","unstructured":"Schmid, M., et al.: Player of Games. CoRR abs\/2112.03178 (2021)"},{"key":"30_CR23","doi-asserted-by":"publisher","first-page":"604","DOI":"10.1038\/s41586-020-03051-4","volume":"588","author":"J Schrittwieser","year":"2020","unstructured":"Schrittwieser, J., et al.: Mastering Atari, go, chess and shogi by planning with a learned model. Nature 588, 604\u2013609 (2020)","journal-title":"Nature"},{"key":"30_CR24","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1038\/nature16961","volume":"529","author":"D Silver","year":"2016","unstructured":"Silver, D., Huang, A., Maddison, C.J., Guez, A., Sifre, L., van den Driessche, G., et al.: Mastering the game of go with deep neural networks and tree search. Nature 529, 484 (2016)","journal-title":"Nature"},{"key":"30_CR25","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1038\/nature24270","volume":"550","author":"D Silver","year":"2017","unstructured":"Silver, D., Schrittwieser, J., Simonyan, K., Antonoglou, I., Huang, A., Guez, A., et al.: Mastering the game of go without human knowledge. Nature 550, 354 (2017)","journal-title":"Nature"},{"issue":"1","key":"30_CR26","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1287\/ited.4.1.48","volume":"4","author":"M Sniedovich","year":"2003","unstructured":"Sniedovich, M.: OR\/MS games: 4. the joy of egg-dropping in Braunschweig and Hong Kong. Inf. Trans. Edu. 4(1), 48\u201364 (2003)","journal-title":"Inf. Trans. Edu."},{"key":"30_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/BFb0054166","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Stevens","year":"1998","unstructured":"Stevens, P., Stirling, C.: Practical model-checking using games. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 85\u2013101. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0054166"},{"issue":"1","key":"30_CR28","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/S0304-3975(01)00185-2","volume":"275","author":"I Walukiewicz","year":"2002","unstructured":"Walukiewicz, I.: Monadic second-order logic on tree-like structures. Theoret. Comput. Sci. 275(1), 311\u2013346 (2002)","journal-title":"Theoret. Comput. Sci."},{"key":"30_CR29","doi-asserted-by":"publisher","DOI":"10.1017\/S026988892000020X","volume":"35","author":"R Xu","year":"2020","unstructured":"Xu, R., Lieberherr, K.J.: Learning self-play agents for combinatorial optimization problems. Knowl. Eng. Rev. 35, e11 (2020)","journal-title":"Knowl. Eng. Rev."}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-06773-0_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T11:12:13Z","timestamp":1659352333000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-06773-0_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031067723","9783031067730"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-06773-0_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"20 May 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Pasadena, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 May 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 May 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/shemesh.larc.nasa.gov\/nfm2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"118","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6.3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}