conference paper published yes Par Alizadeh Alamdari author Guy Avni author 463C8BC2-F248-11E8-B48F-1D18A9856A870000-0001-5588-8287 Thomas A Henzinger author 40876CD8-F248-11E8-B48F-1D18A9856A870000-0002-2985-7724 Anna Lukina author CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425 ToHe department FMCAD: Formal Methods in Computer-Aided Design Formal methods for the design and analysis of complex systems project Machine learning and formal methods have complimentary benefits and drawbacks. In this work, we address the controller-design problem with a combination of techniques from both fields. The use of black-box neural networks in deep reinforcement learning (deep RL) poses a challenge for such a combination. Instead of reasoning formally about the output of deep RL, which we call the wizard, we extract from it a decision-tree based model, which we refer to as the magic book. Using the extracted model as an intermediary, we are able to handle problems that are infeasible for either deep RL or formal methods by themselves. First, we suggest, for the first time, a synthesis procedure that is based on a magic book. We synthesize a stand-alone correct-by-design controller that enjoys the favorable performance of RL. Second, we incorporate a magic book in a bounded model checking (BMC) procedure. BMC allows us to find numerous traces of the plant under the control of the wizard, which a user can use to increase the trustworthiness of the wizard and direct further training. https://research-explorer.ista.ac.at/download/9040/9109/2020_FMCAD_Alamdari.pdf application/pdfno TU Wien Academic Press2020Online Conference eng 2708-7824 978385448042610.34727/2020/isbn.978-3-85448-042-6_21 138-147 Alamdari, P. A., Avni, G., Henzinger, T. A., &#38; Lukina, A. (2020). Formal methods with a touch of magic. In <i>Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design</i> (pp. 138–147). Online Conference: TU Wien Academic Press. <a href="https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_21">https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_21</a> P.A. Alamdari, G. Avni, T.A. Henzinger, A. Lukina, in:, Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design, TU Wien Academic Press, 2020, pp. 138–147. P. A. Alamdari, G. Avni, T. A. Henzinger, and A. Lukina, “Formal methods with a touch of magic,” in <i>Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design</i>, Online Conference, 2020, pp. 138–147. Alamdari PA, Avni G, Henzinger TA, Lukina A. 2020. Formal methods with a touch of magic. Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design. FMCAD: Formal Methods in Computer-Aided Design, 138–147. Alamdari PA, Avni G, Henzinger TA, Lukina A. Formal methods with a touch of magic. In: <i>Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design</i>. TU Wien Academic Press; 2020:138-147. doi:<a href="https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_21">10.34727/2020/isbn.978-3-85448-042-6_21</a> Alamdari, Par Alizadeh, Guy Avni, Thomas A Henzinger, and Anna Lukina. “Formal Methods with a Touch of Magic.” In <i>Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design</i>, 138–47. TU Wien Academic Press, 2020. <a href="https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_21">https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_21</a>. Alamdari, Par Alizadeh, et al. “Formal Methods with a Touch of Magic.” <i>Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design</i>, TU Wien Academic Press, 2020, pp. 138–47, doi:<a href="https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_21">10.34727/2020/isbn.978-3-85448-042-6_21</a>. 90402021-01-24T23:01:10Z2025-07-10T12:01:32Z