=Paper=
{{Paper
|id=Vol-2987/xcoverpage
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-2987/xcoverpage.pdf
|volume=Vol-2987
}}
==None==
https://ceur-ws.org/Vol-2987/xcoverpage.pdf
Dario Della Monica
Gian Luca Pozzato
Enrico Scala
(eds.)
Formal Methods for AI
3rd Workshop on
Artificial Intelligence and
Formal Verification, Logics, Automata and Synthesis
Padua (Italy), September 22, 2021
hosted by the
The Twelfth International Symposium on Games, Automata,
Logics, and Formal Verification
GandALF 2021
Proceedings
Formal Methods for AI
Proceedings of the Dario Della Monica
3rd Workshop on Gian Luca Pozzato
Artificial Intelligence and Enrico Scala
Formal Verification, Logics, Automata and Synthesis (eds.)
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
Chairs
Dario Della Monica University of Udine, Italy
Gian Luca Pozzato University of Turin, Italy
Enrico Scala University of Brescia, Italy
Program Committee
Alessandro Artale Free University of Bozen-Bolzano, Italy
Davide Bresolin University of Padova, Italy
Luca Geatti University of Udine, Italy
Nicola Gigante Free University of Bozen-Bolzano, Italy
Laura Giordano Università del Piemonte Orientale, Italy
Ivan Lanese University of Bologna, Italy
Federico Mari University of Rome Foro Italico, Rome, Italy
Andrea Micheli Fondazione Bruno Kessler, Trento, Italy
Fabio Mogavero University of Naples Federico II, Naples, Italy
Laura Nenzi University of Trieste, Italy
AndreA Orlandini ISTC-CNR, Rome, Italy
Gennaro Parlato University of Molise, Italy
Adriano Peron University of Naples Federico II, Naples, Italy
Gabriele Puppis University of Udine, Italy
Guido Sciavicco University of Ferrara, Italy
Stefano Tonetta Fondazione Bruno Kessler, Trento, Italy
Enrico Tronci University of Rome La Sapienza, Rome, Italy
Tiziano Villa University of Verona, Italy
Enea Zaffanella University of Parma, Italy
Matteo Zavatteri University of Verona, Italy
Technical Advisor
Nicola Gigante Free University of Bozen-Bolzano, Italy
Contents
Preface
Technical Track
Planning with Global State Constraints for Urban Traffic Control
Franc Ivankovic, Marco Roveri . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1
BLACK: A Fast, Flexible and Reliable LTL Satisfiability Checker
Luca Geatti, Nicola Gigante, Angelo Montanari . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
Automated Planning Through Program Verification
Salvatore La Torre, Gennaro Parlato . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
Rule-based Shield Synthesis for Partially Observable Monte Carlo Planning
Giulio Mazzi, Alberto Castellini, Alessandro Farinelli . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19
Dynamic Attack Trees
Aliyu Tanko Ali, Damas Gruska . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
Mining Temporal Networks: Results and Open Problems
Guido Sciavicco, Tiziano Villa, Matteo Zavatteri . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
Multi-Frame Modal Symbolic Learning
Giovanni Pagliarini, Guido Sciavicco, Ionel Eduard Stan . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
Automated Reasoning for Reinforcement Learning Agents in Structured Environments
Alessandro Gianola, Marco Montali, Matteo Papini . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
Using Directional Arc Consistency with Asynchronous Forward-Bounding algorithm
Rachid Adrdor, Lahcen Koutti . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
Statistical Model Checking for the Analysis of Mission- and Safety-Critical
Cyber-Physical Systems
Angela Pappagallo. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
On the Parameterized Verification of Abstract Models of Contact Tracing Protocols
Sylvain Conchon, Giorgio Delzanno, Arnaud Sangnier . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
Towards Learning From Graph Representable Formal Models
Marco Sälzer, Georg Siebert . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
A Software Tool for the Formal Synthesis of Lyapunov Functions and Barrier
Certificates using Neural Networks
Alessandro Abate, Daniele Ahmed, Alec Edwards, Mirco Giacobbe, Andrea Peruffo . . . . . . . . . . . . . . . 73
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 Zaffanella . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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