Luca Geatti Guido Sciavicco Alessandro Umbrico (eds.) Formal Methods for AI 4th Workshop on Artificial Intelligence and Formal Verification, Logics, Automata and Synthesis Udine (Italy), November 28, 2022 hosted by the The 21st International Conference of the Italian Association for Artificial Intelligence AIxIA 2022 Proceedings Formal Methods for AI Proceedings of the Luca Geatti 4th Workshop on Guido Sciavicco Artificial Intelligence and Alessandro Umbrico Formal Verification, Logics, Automata and Synthesis (eds.) Udine (Italy), November 28, 2022 https://overlay.uniud.it/workshop/2022 Copyright © 2022 for the individual papers by the papers’ authors. Copyright © 2022 for the volume as a collection by its editors. This volume and its papers are published under the Creative Commons License Attribution 4.0 International (CC BY 4.0). Workshop organization Chairs Luca Geatti University of Udine, Italy Guido Sciavicco University of Ferrara, Italy Alessandro Umbrico ISTC-CNR, Rome, Italy Program Committee Riccardo De Benedictis CNR-ISTC, Rome, Italy Davide Bresolin University of Padua, Italy Marco Esposito Sapienza University of Rome, Italy Francesco Fabiano University of Parma, Italy Marco Gavanelli University of Parma, Italy Alessandro Gianola Free University of Bozen-Bolzano, Italy Nicola Gigante Free University of Bozen-Bolzano, Italy Federico Mari University of Rome Foro Italico, Italy Andrea Micheli Fondazione Bruno Kessler, Trento, Italy Emilio Munoz-Velasco University of Malaga, Spain Adriano Peron University of Naples Federico II, Italy Raine Ronnholm University of Tampere, Finland Enrico Scala University of Brescia, Italy Mauro Vallati University of Huddersfield, United Kingdom Martin Zimmermann Aalborg University, Denmark Technical Advisor Nicola Gigante Free University of Bozen-Bolzano, Italy Contents Preface Technical Track Neural Network Verification with DSE Benedikt Böing, Falk Howar, Jelle Hüntelmann, Emmanuel Müller, Richard Stewing . . . . . . . . . . . . . . 1 Constrained Training of Neural Networks via Theorem Proving Mark Chevallier, Matthew Whyte, Jacques Fleuriot . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 LTL Modulo Theories over Finite Traces: Modeling, Verification, Open Questions Alessandro Gianola, Nicola Gigante . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 Formally Reasoning about Strategies in Mechanisms Munyque Mittelmann . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 Dynamic Controllability of Temporal Networks via Supervisory Control Matteo Zavatteri, Davide Bresolin, Romeo Rizzi, Tiziano Villa . . . . . . . . . . . . . . . . . . . . . . . . . 27 DELPHIC: Towards an Efficient Possibility-based Epistemic Planning Framework Alessandro Burigana, Paolo Felli, Marco Montali . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Reasoning about Reachability and Concurrency in DEL Games Silvia Stranieri . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 Formal Methods Meet XAI: the Tool DEGARI 2.0 for Social Inclusion Antonio Lieto, Gian Luca Pozzato, Manuel Striani, Stefano Zoia, Rossana Damiano . . . . . . . . . . . . . . 45 An Application of Reinforcement Learning in Industrial Cyber-Physical Systems David Heik, Fouad Bahrpeyma, Dirk Reichelt . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 Regression Trees for System Models and Prediction Swantje Plambeck, Görschwin Fey . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 Formal Certification of Surrogate Models for Cyber-Physical Systems Verification Marco Esposito, Leonardo Picchiami . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 Uniform Interpolation for the Automated Verification of Data-Aware Business Processes Alessandro Gianola . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 Multi-Models and Multi-Formulas Finite Model Checking for Modal Logic Formulas Induction Mauro Milella, Giovanni Pagliarini, Andrea Paradiso, Ionel Eduard Stan . . . . . . . . . . . . . . . . . . . . 81 A Modular SMT-based Approach for Data-aware Conformance Checking Paolo Felli, Alessandro Gianola, Marco Montali, Andrey Rivkin, Sarah Winkler. . . . . . . . . . . . . . . . . 87 From POMDP Executions to Probabilistic Axioms Daniele Meli, Giulio Mazzi, Alberto Castellini, Alessandro Farinelli . . . . . . . . . . . . . . . . . . . . . . . 93