Abstract

hosted by the Bolzano Summer of Knowledge 2020

-

Formal Methods for AI Proceedings

Proceedings of the

2nd Workshop on

Artificial Intelligence and

Formal Verification, Logics, Automata and Synthesis

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

Free University of Bozen-Bolzano, Italy

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

References