Formal Methods for AI
Proceedings Proceedings of the 3rd Workshop on Artificial Intelligence and Formal Verification, Logics, Automata and Synthesis Padua (Italy), September 22, 2021 https://overlay.uniud.it/workshop/2021 Copyright © 2021 for the individual papers by the papers’ authors. Copyright © 2021 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
Dario Della Monica Gian Luca Pozzato Enrico Scala University of Udine, Italy University of Turin, Italy University of Brescia, Italy
Alessandro Artale Davide Bresolin Luca Geatti Nicola Gigante Laura Giordano Ivan Lanese Federico Mari Andrea Micheli Fabio Mogavero Laura Nenzi AndreA Orlandini Gennaro Parlato Adriano Peron Gabriele Puppis Guido Sciavicco Stefano Tonetta Enrico Tronci Tiziano Villa Enea Zaffanella Matteo Zavatteri
Nicola Gigante
Free University of Bozen-Bolzano, Italy University of Padova, Italy University of Udine, Italy Free University of Bozen-Bolzano, Italy Università del Piemonte Orientale, Italy University of Bologna, Italy University of Rome Foro Italico, Rome, Italy Fondazione Bruno Kessler, Trento, Italy University of Naples Federico II, Naples, Italy University of Trieste, Italy ISTC-CNR, Rome, Italy University of Molise, Italy University of Naples Federico II, Naples, Italy University of Udine, Italy University of Ferrara, Italy Fondazione Bruno Kessler, Trento, Italy University of Rome La Sapienza, Rome, Italy University of Verona, Italy University of Parma, Italy University of Verona, Italy
Free University of Bozen-Bolzano, Italy Preface Technical Track Planning with Global State Constraints for Urban Trac Control Franc Ivankovic, Marco Roveri . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 BLACK: A Fast, Flexible and Reliable LTL Satisfiability Checker Luca Geatti, Nicola Gigante, Angelo Montanari . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 Rule-based Shield Synthesis for Partially Observable Monte Carlo Planning Giulio Mazzi, Alberto Castellini, Alessandro Farinelli . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Mining Temporal Networks: Results and Open Problems Guido Sciavicco, Tiziano Villa, Matteo Zavatteri. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Ranking Model Checking Backends for Automated Selection via Classification and Regression Learning Jannik Dunkelau, Leo Baldus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 Preferential Reasoning with Typicality and Neural Network Models (Extended Abstract) Laura Giordano, Valentina Gliozzi, Daniele Theseider Dupré . . . . . . . . . . . . . . . . . . . . . . . . . . 83 Reverse engineering with P-stable Abstractions Anna Becchi, Alessandro Cimatti, Enea Zaanella . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 AI-guided optimal deployments of drone-intercepting systems in large critical areas Marco Esposito . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 QUGA - Quality Guarantees for Autoencoders Benedikt Böing, Rajarshi Roy, Daniel Neider, Emmanuel Müller . . . . . . . . . . . . . . . . . . . . . . . . 103 Simulation-Based Synthesis of Personalised Therapies for Colorectal Cancer Marco Esposito, Leonardo Picchiami . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 109