Riccardo De Benedictis Luca Geretti Andrea Micheli (eds.) Formal Methods for AI 2nd Workshop on Artificial Intelligence and Formal Verification, Logics, Automata and Synthesis September 25, 2020 hosted by the Bolzano Summer of Knowledge 2020 Proceedings Formal Methods for AI Proceedings of the Riccardo De Benedictis 2nd Workshop on Luca Geretti Artificial Intelligence and Andrea Micheli Formal Verification, Logics, Automata and Synthesis (eds.) September 25, 2020 https://overlay.uniud.it/workshop/2020 Copyright © 2020 for the individual papers by the papers’ authors. Copyright © 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 Chairs Riccardo De Benedictis ISTC - National Research Council, Rome, Italy Luca Geretti University of Verona, Italy Andrea Micheli Fondazione Bruno Kessler, Trento, Italy Program Committee Massimo Benerecetti University of Naples Federico II, Italy Davide Bresolin University of Padova, Italy Amedeo Cesta ISTC - National Research Council, Rome, Italy Dario Della Monica University of Udine, Italy Marco Faella University of Naples Federico II, Italy Nicola Gigante Free University of Bozen-Bolzano, Italy Salvatore La Torre University of Salerno, Italy Ivan Lanese University of Bologna, Italy Federico Mari University of Rome Foro Italico, Italy Angelo Montanari University of Udine, Italy AndreA Orlandini ISTC - National Research Council, Rome, 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, Trento, Italy Enrico Tronci University of Rome La Sapienza, Italy Alessandro Umbrico ISTC - National Research Council, Rome, Italy Tiziano Villa University of Verona, Italy Technical Advisor Nicola Gigante Free University of Bozen-Bolzano, Italy Contents Preface Invited Talk Verifying Autonomous Robots: Challenges and Reflections Clare Dixon . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 Technical Track Symbolic Learning with Interval Temporal Logic: the Case of Regression Estrella Lucena-Sanchez, Guido Sciavicco, Ionel Eduard Stan . . . . . . . . . . . . . . . . . . . . . . . . . . 5 A Note on Ultimately-Periodic Finite Interval Temporal Logic Model Checking Dario Della Monica, Angelo Montanari, Guido Sciavicco, Ionel Eduard Stan . . . . . . . . . . . . . . . . . . 11 Theorem Proving for Non-normal Modal Logics Tiziano Dalmonte, Sara Negri, Nicola Olivetti, Gian Luca Pozzato . . . . . . . . . . . . . . . . . . . . . . . 17 Finite vs. Infinite Traces in Temporal Logics Alessandro Artale and Andrea Mazzullo, Ana Ozaki . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 A kernel function for Signal Temporal Logic formulae Luca Bortolussi, Giuseppe Maria Gallo, Laura Nenzi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Reasoning in Multi-Agent Conformant Planning over Transition Systems Peipei Wu, Yanjun Li . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Optimal Fault-Tolerant Relay Node Positioning in Critical Wireless Networks via Artificial Intelligence Qian Matteo Chen , Toni Mancini , Igor Melatti , Enrico Tronci , Alberto Finzi . . . . . . . . . . . . . . . . 41 A Fixed-point Model-checker for BDI Logics over Finite-state Worlds Salvatore La Torre, Gennaro Parlato . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 A Language for Timeline-based Planning Giulio Bernardi, Amedeo Cesta, Andrea Orlandini, Alessandro Umbrico, Marta Cialdea Mayer . . . . . . . . 53 AI-Guided Synthesis of Personalised Pharmacological Treatments via In Silico Clinical Trials S. Sinisi, V. Alimguzhin, T. Mancini, E. Tronci, F. Mari, B. Leeners . . . . . . . . . . . . . . . . . . . . . 59 On the Formalization of Decentralized Contact Tracing Protocols P. A. Abdulla, M. F. Atig, G. Delzanno, M. Montali, A. Sangnier . . . . . . . . . . . . . . . . . . . . . . . 65 Electricity Network Constraint Management using Individualised Demand Aware Price Policies I. Melatti , V. Alimguzhin , F. Mari , M. Prodanovic , B. Hayes . . . . . . . . . . . . . . . . . . . . . . . . 71 Adversarial Learning of Robust and Safe Controllers for Cyber-Physical Systems Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, Francesco Franchina . . . . . . . . . . . . . . . . . . . 77 Learning How to Monitor: Pairing Monitoring and Learning for Online System Verification Andrea Brunello, Dario Della Monica, Angelo Montanari, Andrea Urgolo . . . . . . . . . . . . . . . . . . . 83 Formal Runtime Monitoring Approaches for Autonomous Vehicles Saumya Shankar, Ujwal V R, Srinivas Pinisetty, Partha Roop . . . . . . . . . . . . . . . . . . . . . . . . . 89 Bayesian Neural Predictive Monitoring Luca Bortolussi, Francesca Cairoli, Nicola Paoletti, S.A. Smolka, S.D. Stoller . . . . . . . . . . . . . . . . . 95