Formal Methods for AI
Proceedings Proceedings of the 5th Workshop on Artificial Intelligence and Formal Verification, Logics, Automata and Synthesis Rome (Italy), November 7, 2023 https://overlay.uniud.it/workshop/2023 Copyright © 2024 for the individual papers by the papers’ authors. Copyright © 2024 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
Andrea Brunello Alessandro Gianola Fabio Mogavero
University of Udine, Italy INESC-ID / IST, Universidade de Lisboa, Portugal University of Napoli Federico II, Italy Andrea Brunello Alessandro Gianola Fabio Mogavero (eds.)
Dylan Bellier Massimo Benerecetti Laura Bozzelli Dario Della Monica Daniele Dell’Erba Marco Faella Luca Geatti Silvio Ghilardi Nicola Gigante Inês Lynce Andrea Mazzullo Andrea Micheli AndreA Orlandini Matteo Papini Gian Luca Pozzato Guido Sciavicco Nicola Saccomanno Ionel Eduard Stan Cesare Tinelli Tiziano Villa
Zavatteri Matteo
Nicola Gigante
University of Rennes, France University of Napoli Federico II, Italy University of Napoli Federico II, Italy University of Udine, Italy University of Liverpool, UK University of Napoli Federico II, Italy University of Udine, Italy University of Milan, Italy Free University of Bozen-Bolzano, Italy INESC-ID / IST, Universidade de Lisboa, Portugal University of Trento, Italy Fondazione Bruno Kessler, Trento, Italy ISTC-CNR, Rome, Italy Universitat Pompeu Fabra, Barcelona, Spain University of Turin, Italy University of Ferrara, Italy University of Udine, Italy Free University of Bozen-Bolzano, Italy The University of Iowa, USA University of Verona, Italy University of Padova, Italy Free University of Bozen-Bolzano, Italy
Technical Track Formal Design of Cyber-Physical Systems with Learning-Enabled Components Thao Dang . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 On Challenges and Opportunities in the Translation of Deep Neural Networks into Finite Automata Marco Sälzer, Eric Alsmann and Martin Lange . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 Towards Machine Learning enhanced LTL Monitoring Luca Geatti, Angelo Montanari and Nicola Saccomanno . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 Towards Large Language Model Architectures for Knowledge Acquisition and Strategy Synthesis Paolo Giorgini, Andrea Mazzullo, Marco Robol and Marco Roveri . . . . . . . . . . . . . . . . . . . . . . . . 21 ODD-based Health Monitoring and Predictive Maintenance of Degrading Vehicle Functionality Yannick Kees, Gerald Sauter, Ryan Mut, Benedikt Franke, Frank Köster and Sven Hallerbach . . . . . . . . . 31 Composition of Nondeterministic Services for LTLf Task Specification Giuseppe De Giacomo, Marco Favorito and Luciana Silo . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 Tree Kernels to Support Formal Methods-based Testing of Evolving Specifications Francesco Altiero, Anna Corazza, Sergio Di Martino, Adriano Peron and Luigi Libero Lucio Starace . . . . . A Landscape of First-Order Linear Temporal Logics in Infinite-State Verification and Temporal Ontologies Alessandro Artale, Luca Geatti, Nicola Gigante and Andrea Mazzullo . . . . . . . . . . . . . . . . . . . . . . Clock Specifications for Temporal Tasks in Planning and Learning Giuseppe De Giacomo, Marco Favorito and Fabio Patrizi . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 85