Papers

The papers I've written.

2026

• Time Robustness for Point-Based Semantics of Metric Interval Temporal Logic

  International Conference on Principles of Knowledge Representation and Reasoning (KR) · pp. 589–599

  Simone Silvetti, Ivan Compagnucci, Francesca Cairoli, Catia Trubiani, Laura Nenzi

  A quantitative notion of time robustness for MITL over timestamped events, stable under small timing perturbations.

2025

• Guided by Stars: Interpretable Concept Learning Over Time Series via Temporal Logic Semantics

  arXiv preprint arXiv:2511.04244

  Irene Ferfoglia, Simone Silvetti, Gaia Saveri, Laura Nenzi, Luca Bortolussi

  STELLE: a neuro-symbolic time series classifier whose predictions come with human-readable temporal logic explanations.

• Modular and Online Monitoring of Temporal Logic Specification with Integral and Filter

  International Conference on Runtime Verification (RV) · pp. 120–139

  Simone Silvetti, Michele Loreti, Laura Nenzi

  Extending an STL-based specification language with sliding-window integrals and filters, plus an efficient online monitor.

• Towards Interpretable Concept Learning over Time Series via Temporal Logic Semantics

  arXiv preprint arXiv:2508.03269

  Irene Ferfoglia, Simone Silvetti, Gaia Saveri, Laura Nenzi, Luca Bortolussi

  First results on classifying time series through an embedding into Signal Temporal Logic concepts.

• Monitoring Spatially Distributed Cyber-Physical Systems with Alternating Finite Automata

  ACM International Conference on Hybrid Systems: Computation and Control (HSCC) · pp. 1–11

  Anand Balakrishnan, Sheryl Paul, Simone Silvetti, Laura Nenzi, Jyotirmoy V Deshmukh

  An automaton-based semantics for the spatio-temporal logic STREL, to monitor mobile, networked cyber-physical systems.

2024

• Is Machine Learning Model Checking Privacy Preserving?

  International Symposium on Leveraging Applications of Formal Methods (ISoLA) · pp. 139–155

  Luca Bortolussi, Laura Nenzi, Gaia Saveri, Simone Silvetti

  Can a system be queried through learned STL kernels without revealing the system itself? A look at the privacy of ML model checking.

2023

• MoonLight: A Lightweight Tool for Monitoring Spatio-Temporal Properties

  International Journal on Software Tools for Technology Transfer (STTT), 25(4) · pp. 503–517

  Laura Nenzi, Ezio Bartocci, Luca Bortolussi, Simone Silvetti, Michele Loreti

  The journal version of MoonLight: interfaces, scripting language and performance of the spatio-temporal monitoring tool.

2020

• MoonLight: A Lightweight Tool for Monitoring Spatio-Temporal Properties

  International Conference on Runtime Verification (RV) · pp. 417–428

  Ezio Bartocci, Luca Bortolussi, Michele Loreti, Laura Nenzi, Simone Silvetti

  A Java tool for monitoring temporal and spatio-temporal (STREL) properties of mobile, spatially distributed CPS.

2019

• A Logic-Based Learning Approach to Explore Diabetes Patient Behaviors

  International Conference on Computational Methods in Systems Biology (CMSB) · pp. 188–206

  Josephine Lamp, Simone Silvetti, Marc Breton, Laura Nenzi, Lu Feng

  Learning Signal Temporal Logic formulas from real patient data to understand which behaviours affect Type 1 Diabetes control.

• Parametric Verification and Synthesis based on Gaussian Processes

  International Workshop on Synthesis of Complex Parameters (SynCoP)

  Luca Bortolussi, Laura Nenzi, Simone Silvetti

  A review of Gaussian Process and Bayesian optimisation techniques for parameter verification and synthesis of stochastic systems.

2018

• Bayesian Statistical Parametric Verification and Synthesis by Machine Learning

  Winter Simulation Conference (WSC) · pp. 381–394

  Luca Bortolussi, Guido Sanguinetti, Simone Silvetti

  A tutorial on using Gaussian Processes to estimate satisfaction probabilities of stochastic models as a function of their parameters.

• Signal Convolution Logic

  International Symposium on Automated Technology for Verification and Analysis (ATVA) · pp. 267–283

  Simone Silvetti, Laura Nenzi, Ezio Bartocci, Luca Bortolussi

  SCL: a temporal logic with convolutional filters, to reason about the percentage of time a property holds.

• Combining Machine Learning and Formal Methods for Complex Systems Design

  PhD thesis, University of Udine

  Simone Silvetti

  My PhD thesis: machine learning, active learning and optimisation to address the limits of temporal logics and model checking.

• A Robust Genetic Algorithm for Learning Temporal Specifications from Data

  International Conference on Quantitative Evaluation of Systems (QEST) · pp. 323–338

  Laura Nenzi, Simone Silvetti, Ezio Bartocci, Luca Bortolussi

  Mining Signal Temporal Logic requirements from good and anomalous trajectories, learning both structure and parameters.

• Bayesian Statistical Parameter Synthesis for Linear Temporal Properties of Stochastic Models

  International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) · pp. 396–413

  Luca Bortolussi, Simone Silvetti

  Finding the parameter regions where a stochastic model satisfies a temporal property, with statistical guarantees, via Gaussian Processes and active learning.

2017

• An Active Learning Approach to the Falsification of Black Box Cyber-Physical Systems

  International Conference on Integrated Formal Methods (iFM) · pp. 3–17

  Simone Silvetti, Alberto Policriti, Luca Bortolussi

  Using active learning to falsify temporal properties of black box cyber-physical systems with far fewer simulations.

2016

• Logic-Based Multi-Objective Design of Chemical Reaction Networks

  International Workshop on Hybrid Systems Biology (HSB) · pp. 164–178

  Luca Bortolussi, Alberto Policriti, Simone Silvetti

  Tuning the parameters of stochastic models so that several Signal Temporal Logic goals hold at once, for synthetic biology design.