Formal Methods for AI Proceedings
4th Workshop on Artificial Intelligence and Formal Verification, Logics, Automata and Synthesis 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
Davide Bresolin Marco Esposito Francesco Fabiano Marco Gavanelli Alessandro Gianola Nicola Gigante Federico Mari Andrea Micheli Emilio Munoz-Velasco Adriano Peron Raine Ronnholm Enrico Scala Mauro Vallati
Martin Zimmermann
University of Padua, Italy Sapienza University of Rome, Italy University of Parma, Italy University of Parma, Italy Free University of Bozen-Bolzano, Italy Free University of Bozen-Bolzano, Italy University of Rome Foro Italico, Italy Fondazione Bruno Kessler, Trento, Italy University of Malaga, Spain University of Naples Federico II, Italy University of Tampere, Finland University of Brescia, Italy University of Huddersfield, United Kingdom Aalborg University, Denmark
Technical Track
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 Eficient 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 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