=Paper=
{{Paper
|id=Vol-3311/xcoverpage
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-3311/xcoverpage.pdf
|volume=Vol-3311
}}
==None==
<pdf width="1500px">https://ceur-ws.org/Vol-3311/xcoverpage.pdf</pdf>
<pre>
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

</pre>