co-located with the 18th International Conference of the Italian Association for Artificial Intelligence (AI*IA 2019)
Formal Methods for AI Proceedings
1st Workshop on Artificial Intelligence and Formal Verification, Logics, Automata and Synthesis Rende, Italy, November 19–20, 2019 https://overlay.uniud.it/workshop/2019 Copyright c 2020 for the individual papers by the papers’ authors. Copyright c 2020 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
Nicola Gigante Federico Mari
AndreA Orlandini
University of Rome Foro Italico, Italy
ISTC - National Research Council, Rome, Italy Massimo Benerecetti University of Naples Federico II, Italy Davide Bresolin University of Padova, Italy Amedeo Cesta ISTC - National Research Council, Rome, Italy Alessandro Cimatti Fondazione Bruno Kessler, Trento, Italy Riccardo De Benedictis ISTC - National Research Council, Rome, Italy Dario Della Monica University of Udine, Italy Marco Faella University of Naples Federico II, Italy Luca Geretti University of Verona, Italy Salvatore La Torre University of Salerno, Italy Ivan Lanese University of Bologna, Italy Angelo Montanari University of Udine, Italy Adriano Peron University of Naples Federico II, Italy Carla Piazza University of Udine, Italy Pietro Sala University of Verona, Italy Guido Sciavicco University of Ferrara, Italy Stefano Tonetta Fondazione Bruno Kessler, Italy Enrico Tronci Sapienza University of Rome, Italy Alessandro Umbrico ISTC - National Research Council, Rome, Italy Tiziano Villa University of Verona, Italy
Preface
Towards Verifiable and Safe Model-Free Reinforcement Learning Mohammadhosein Hasanbeig, Daniel Kroening, Alessandro Abate . . . . . . . . . . . . . . . . . . . . . . . . 1
Model Checking BDI Logics over Finite-state Worlds Salvatore La Torre, Gennaro Parlato . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 In Silico Clinical Trials through AI and Statistical Model Checking Vadim Alimguzhin, Toni Mancini, Annalisa Massini, Stefano Sinisi, Enrico Tronci . . . . . . . . . . . . . . 17 Automated Verification of Noisy Nonlinear Cyber-Physical Systems with Ariadne Davide Bresolin, Luca Geretti, Tiziano Villa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Towards Interval Temporal Logic Rule-Based Classification Estrella Lucena-Sánchez, Emilio Mun¨oz-Velasco, Guido Sciavicco, Ionel Eduard Stan, Alessandro Vaccari . . . 65 Strong Controllability of Temporal Networks with Decisions Matteo Zavatteri, Romeo Rizzi, Tiziano Villa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 Complexity of Weak, Strong and Dynamic Controllability of CNCUs Matteo Zavatteri, Romeo Rizzi, Tiziano Villa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 A Prototype for the Robust Execution of Flexible Plans Annarita Lanzilli, Marta Cialdea Mayer, Amedeo Cesta, Andrea Orlandini, Alessandro Umbrico . . . . . . . . 89 Control Software Synthesis for Cyber-Physical Systems with QKS Vadim Alimguzhin, Federico Mari, Igor Melatti . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95 Optimization and Multistage Systems. The Thawing Case Eleonora Pippia, Arianna Bozzato, Emidio Tiberi, Riccardo Furlanetto, Alberto Policriti . . . . . . . . . . . . 101