{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T11:35:02Z","timestamp":1780054502344,"version":"3.54.0"},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,7]]},"abstract":"<jats:p>Recurrent neural networks (RNNs) have emerged as an effective representation of control policies in sequential decision-making problems.\n\nHowever, a major drawback in the application of RNN-based policies is the difficulty in providing formal guarantees on the satisfaction of behavioral specifications, e.g. safety and\/or reachability. \n\nBy integrating techniques from formal methods and machine learning, we propose an approach to automatically extract a finite-state controller (FSC) from an RNN, which, when composed with a finite-state system model, is amenable to existing formal verification tools.\n\nSpecifically, we introduce an iterative modification to the so-called quantized bottleneck insertion technique to create an FSC as a randomized policy with memory.\n\nFor the cases in which the resulting FSC fails to satisfy the specification, verification generates diagnostic information.\n\nWe utilize this information to either adjust the amount of memory in the extracted FSC or perform focused retraining of the RNN.\n\nWhile generally applicable, we detail the resulting iterative procedure in the context of policy synthesis for partially observable Markov decision processes (POMDPs), which is known to be notoriously hard.\n\nThe numerical experiments show that the proposed approach outperforms traditional POMDP synthesis methods by 3 orders of magnitude within 2% of optimal benchmark values.<\/jats:p>","DOI":"10.24963\/ijcai.2020\/570","type":"proceedings-article","created":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T12:12:10Z","timestamp":1594210330000},"page":"4121-4127","source":"Crossref","is-referenced-by-count":24,"title":["Verifiable RNN-Based Policies for POMDPs Under Temporal Logic Constraints"],"prefix":"10.24963","author":[{"given":"Steven","family":"Carr","sequence":"first","affiliation":[{"name":"University of Texas at Austin"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nils","family":"Jansen","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ufuk","family":"Topcu","sequence":"additional","affiliation":[{"name":"University of Texas at Austin"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"10584","event":{"name":"Twenty-Ninth International Joint Conference on Artificial Intelligence and Seventeenth Pacific Rim International Conference on Artificial Intelligence {IJCAI-PRICAI-20}","theme":"Artificial Intelligence","location":"Yokohama, Japan","acronym":"IJCAI-PRICAI-2020","number":"28","sponsor":["International Joint Conferences on Artificial Intelligence Organization (IJCAI)"],"start":{"date-parts":[[2020,7,11]]},"end":{"date-parts":[[2020,7,17]]}},"container-title":["Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence"],"original-title":[],"deposited":{"date-parts":[[2020,7,9]],"date-time":"2020-07-09T02:16:01Z","timestamp":1594260961000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.ijcai.org\/proceedings\/2020\/570"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2020,7]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/ijcai.2020\/570","relation":{},"subject":[],"published":{"date-parts":[[2020,7]]}}}