EDBT 2026 Demo / reviewers in the wild / expert
Luca Bortolussi
dblp:32/1171
· DBLP profile ↗
74ranked-venue papers
28as first author
31since 2021 · last 2026
0000-0001-8874-4001ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 29 · 10 first-author · 15 since 2021Theory of computation · 27 · 14 first-author · 4 since 2021Artificial intelligence and machine learning · 15 · 1 first-author · 13 since 2021Systems, architecture and hardware · 7 · 3 first-author · 1 since 2021Graphics, computer vision, multimedia, augmented reality and games · 4 · 4 since 2021Databases, data management, data science and information retrieval · 2 · 2 since 2021Applied, interdisciplinary, general and emerging computing · 2 · 1 first-authorSecurity and privacy · 1 · 1 first-author
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | Graph-Conditional Flow Matching for Relational Data GenerationabstractData synthesis is gaining momentum as a privacy-enhancing technology. While single-table tabular data generation has seen considerable progress, current methods for multi-table data often lack the flexibility and expressiveness needed to capture complex relational structures. In particular, they struggle with long-range dependencies and complex foreign-key relationships, such as tables with multiple parent tables or multiple types of links between the same pair of tables. We propose a generative model for relational data that generates the content of a relational dataset given the graph formed by the foreign-key relationships. We do this by learning a deep generative model of the content of the whole relational database by flow matching, where the neural network trained to denoise records leverages a graph neural network to obtain information from connected records. Our method is flexible, as it can support relational datasets with complex structures, and expressive, as the generation of each record can be influenced by any other record within the same connected component. We evaluate our method on several benchmark datasets and show that it achieves state-of-the-art performance in terms of synthetic data fidelity. Davide Scassola, Sebastiano Saccani, Luca Bortolussi |
AAAI | 3 |
| 2026 | DeGAS: Gradient-Based Optimization of Probabilistic Programs without SamplingabstractWe present DeGAS, a differentiable Gaussian approximate semantics for loopless probabilistic programs that enables sample-free, gradient-based optimization in models with both continuous and discrete components. DeGAS evaluates programs under a Gaussian-mixture semantics and replaces measure-zero predicates and discrete branches with a vanishing smoothing, yielding closed-form expressions for posterior and path probabilities. We prove differentiability of these quantities with respect to program parameters, enabling end-to-end optimization via standard automatic differentiation, without Monte Carlo estimators. On thirteen benchmark programs, DeGAS achieves accuracy and runtime competitive with variational inference and MCMC. Importantly, it reliably tackles optimization problems where sampling-based baselines fail to converge due to conditioning involving continuous variables. Francesca Randone, Romina Doz, Mirco Tribastone, Luca Bortolussi |
TACAS (1) | 4 |
| 2025 | Zero-Shot Conditioning of Score-Based Diffusion Models by Neuro-Symbolic ConstraintsabstractScore-based diffusion models have emerged as effective approaches for both conditional and unconditional generation. Still conditional generation is based on either a specific training of a conditional model or classifier guidance, which requires training a noise-dependent classifier, even when a classifier for uncorrupted data is given. We propose a method that, given a pre-trained unconditional score-based generative model, samples from the conditional distribution under arbitrary logical constraints, without requiring additional training. Differently from other zero-shot techniques, that rather aim at generating valid conditional samples, our method is designed for approximating the true conditional distribution. Firstly, we show how to manipulate the learned score in order to sample from an un-normalized distribution conditional on a user-defined constraint. Then, we define a flexible and numerically stable neuro-symbolic framework for encoding soft logical constraints. Combining these two ingredients we obtain a general, but approximate, conditional sampling algorithm. We further developed effective heuristics aimed at improving the approximation. Finally, we show the effectiveness of our approach in approximating conditional distributions for various types of constraints and data: tabular data, images and time series. Davide Scassola, Sebastiano Saccani, Ginevra Carbone, Luca Bortolussi |
AAAI | 4 |
| 2025 | Scaling Combinatorial Optimization Neural Improvement Heuristics with Online Search and AdaptationabstractWe introduce Limited Rollout Beam Search (LRBS), a beam search strategy for deep reinforcement learning (DRL) based combinatorial optimization improvement heuristics. Utilizing pre-trained models on the Euclidean Traveling Salesperson Problem, LRBS significantly enhances both in-distribution performance and generalization to larger problem instances, achieving optimality gaps that outperform existing improvement heuristics and narrowing the gap with state-of-the-art constructive methods. We also extend our analysis to two pickup and delivery TSP variants to validate our results. Finally, we employ our search strategy for offline and online adaptation of the pre-trained improvement policy, leading to improved search performance and surpassing recent adaptive methods for constructive heuristics. Federico Julian Camerota Verdù, Lorenzo Castelli, Luca Bortolussi |
AAAI | 3 |
| 2025 | Effective Analog ICs Floorplanning with Relational Graph Neural Networks and Reinforcement LearningabstractAnalog integrated circuit (IC) floorplanning is typically a manual process with the placement of components (devices and modules) planned by a layout engineer. This process is further complicated by the interdependence of floorplanning and routing steps, numerous electric and layout-dependent constraints, as well as the high level of customization expected in analog design. This paper presents a novel automatic floorplanning algorithm based on reinforcement learning. It is augmented by a relational graph convolutional neural network model for encoding circuit features and positional constraints. The combination of these two machine learning methods enables knowledge transfer across different circuit designs with distinct topologies and constraints, increasing the generalization ability of the solution. Applied to 6 industrial circuits, our approach surpassed established floorplanning techniques in terms of speed, area and half-perimeter wire length. When integrated into a procedural generator for layout completion, overall layout time was reduced by 67.3% with a 8.3% mean area reduction compared to manual layout. Davide Basso, Luca Bortolussi, Mirjana S. Videnovic-Misic, Husni Habal |
DATE | 2 |
| 2025 | Evolutionary Synthesis of Probabilistic ProgramsabstractModeling the relationships between variables through probability distributions lies at the core of probabilistic models, enabling reasoning under uncertainty. Probabilistic programming offers an effective way to represent these models by blending the simplicity of standard programming constructs with the power of automatic inference algorithms. The languages for expressing probabilistic programs are augmented with primitives representing various probability distributions to effectively capture the stochastic behavior inherent in the data. However, writing a probabilistic program is hard, because it typically requires prior knowledge about the data generation mechanism. In this work, we propose a framework for automatically synthesizing probabilistic programs directly from data, thereby learning the underlying relationships between variables and the data-generating process. We adopt an evolutionary approach, specifically grammatical evolution (GE), to extensively explore the space of probabilistic programs, aiming to discover the most likely program that describes the observed data. We experimentally evaluate our method across several benchmarks, incorporating varying levels of prior knowledge through a sketching strategy embedded into the grammar fed to GE, to demonstrate the potential of this evolutionary framework. This evaluation highlights the flexibility and effectiveness of GE in synthesizing probabilistic programs under different informational constraints. Romina Doz, Francesca Randone, Eric Medvet, Luca Bortolussi |
GECCO | 4 |
| 2025 | Intrinsic Dimension Correlation: uncovering nonlinear connections in multimodal representationsabstractTo gain insight into the mechanisms behind machine learning methods, it is crucial to establish connections among the features describing data points. However, these correlations often exhibit a high-dimensional and strongly nonlinear nature, which makes them challenging to detect using standard methods. This paper exploits the entanglement between intrinsic dimensionality and correlation to propose a metric that quantifies the (potentially nonlinear) correlation between high-dimensional manifolds. We first validate our method on synthetic data in controlled environments, showcasing its advantages and drawbacks compared to existing techniques. Subsequently, we extend our analysis to large-scale applications in neural network representations. Specifically, we focus on latent representations of multimodal data, uncovering clear correlations between paired visual and textual embeddings, whereas existing methods struggle significantly in detecting similarity. Our results indicate the presence of highly nonlinear correlation patterns between latent manifolds. Lorenzo Basile, Santiago Acevedo, Luca Bortolussi, Fabio Anselmi, Alex Rodriguez |
ICLR | 3 |
| 2025 | Frequency maps reveal the correlation between Adversarial Attacks and Implicit BiasabstractDespite their impressive performance in classification tasks, neural networks are known to be vulnerable to adversarial attacks, subtle perturbations of the input data designed to deceive the model. In this work, we investigate the correlation between these perturbations and the implicit bias of neural networks trained with gradient-based algorithms. To this end, we analyse a representation of the network’s implicit bias through the lens of the Fourier transform. Specifically, we identify unique fingerprints of implicit bias and adversarial attacks by calculating the minimal, essential frequencies needed for accurate classification of each image, as well as the frequencies that drive misclassification in its adversarially perturbed counterpart. This approach enables us to uncover and analyse the correlation between these essential frequencies, providing a precise map of how the network’s biases align or contrast with the frequency components exploited by adversarial attacks. To this end, among other methods, we use a newly introduced technique capable of detecting nonlinear correlations between high-dimensional datasets. Our results provide empirical evidence that the network bias in Fourier space and the target frequencies of adversarial attacks are highly correlated and suggest new potential strategies for adversarial defence. Code is available at https://github.com/lorenzobasile/ImplicitBiasAdversarial Lorenzo Basile, Nikos Karantzas, Alberto d'Onofrio, Luca Manzoni, Luca Bortolussi, Alex Rodriguez, Fabio Anselmi |
IJCNN | 5 |
| 2025 | Bridging Logic and Learning: Decoding Temporal Logic Embeddings via Transformers
Sara Candussio, Gaia Saveri, Gabriele Sarti, Luca Bortolussi |
ECML/PKDD (5) | 4 |
| 2025 | Conformal Predictive Monitoring for Multi-modal Scenarios
Francesca Cairoli, Luca Bortolussi, Jyotirmoy V. Deshmukh, Lars Lindemann, Nicola Paoletti |
RV | 2 |
| 2025 | CoCAI: Copula-Based Conformal Anomaly Identification for Multivariate Time-Series
Nicholas Andrea Pearson, Francesca Zanello, Davide Russo, Luca Bortolussi, Francesca Cairoli |
RV | 4 |
| 2025 | On the Robustness of Bayesian Neural Networks to Adversarial AttacksabstractVulnerability to adversarial attacks is one of the principal hurdles to the adoption of deep learning in safety-critical applications. Despite significant efforts, both practical and theoretical, training deep learning models robust to adversarial attacks is still an open problem. In this article, we analyse the geometry of adversarial attacks in the over-parameterized limit for Bayesian neural networks (BNNs). We show that, in the limit, vulnerability to gradient-based attacks arises as a result of degeneracy in the data distribution, i.e., when the data lie on a lower dimensional submanifold of the ambient space. As a direct consequence, we demonstrate that in this limit, BNN posteriors are robust to gradient-based adversarial attacks. Crucially, by relying on the convergence of infinitely-wide BNNs to Gaussian processes (GPs), we prove that, under certain relatively mild assumptions, the expected gradient of the loss with respect to the BNN posterior distribution is vanishing, even when each NN sampled from the BNN posterior does not have vanishing gradients. The experimental results on the MNIST, Fashion MNIST, and a synthetic dataset with BNNs trained with Hamiltonian Monte Carlo and variational inference support this line of arguments, empirically showing that BNNs can display both high accuracy on clean data and robustness to both gradient-based and gradient-free adversarial attacks. Luca Bortolussi, Ginevra Carbone, Luca Laurenti, Andrea Patanè, Guido Sanguinetti, Matthew Wicker |
IEEE Trans. Neural Networks Learn. Syst. | 1 |
| 2024 | stl2vec: Semantic and Interpretable Vector Representation of Temporal LogicabstractIntegrating symbolic knowledge and data-driven learning algorithms is a longstanding challenge in Artificial Intelligence. Despite the recognized importance of this task, a notable gap exists due to the discreteness of symbolic representations and the continuous nature of machine-learning computations. One of the desired bridges between these two worlds would be to define semantically grounded vector representation (feature embedding) of logic formulae, thus enabling to perform continuous learning and optimization in the semantic space of formulae. We tackle this goal for knowledge expressed in Signal Temporal Logic (STL) and devise a method to compute continuous embeddings of formulae with several desirable properties: the embedding (i) is finite-dimensional, (ii) faithfully reflects the semantics of the formulae, (iii) does not require any learning but instead is defined from basic principles, (iv) is interpretable. Another significant contribution lies in demonstrating the efficacy of the approach in two tasks: learning model checking, where we predict the probability of requirements being satisfied in stochastic processes; and integrating the embeddings into a neuro-symbolic framework, to constrain the output of a deep-learning generative model to comply to a given logical specification. Gaia Saveri, Laura Nenzi, Luca Bortolussi, Jan Kretínský |
ECAI | 3 |
| 2024 | Is Machine Learning Model Checking Privacy Preserving?
Luca Bortolussi, Laura Nenzi, Gaia Saveri, Simone Silvetti |
ISoLA (2) | 1 |
| 2024 | Towards a Probabilistic Programming Approach to Analyse Collective Adaptive Systems
Francesca Randone, Romina Doz, Francesca Cairoli, Luca Bortolussi |
ISoLA (1) | 4 |
| 2024 | ECATS: Explainable-by-Design Concept-Based Anomaly Detection for Time Series
Irene Ferfoglia, Gaia Saveri, Laura Nenzi, Luca Bortolussi |
NeSy (2) | 4 |
| 2024 | Retrieval-Augmented Mining of Temporal Logic Specifications from Data
Gaia Saveri, Luca Bortolussi |
ECML/PKDD (7) | 2 |
| 2024 | Inference of Probabilistic Programs with Moment-Matching Gaussian MixturesabstractComputing the posterior distribution of a probabilistic program is a hard task for which no one-fit-for-all solution exists. We propose Gaussian Semantics, which approximates the exact probabilistic semantics of a bounded program by means of Gaussian mixtures. It is parametrized by a map that associates each program location with the moment order to be matched in the approximation. We provide two main contributions. The first is a universal approximation theorem stating that, under mild conditions, Gaussian Semantics can approximate the exact semantics arbitrarily closely. The second is an approximation that matches up to second-order moments analytically in face of the generally difficult problem of matching moments of Gaussian mixtures with arbitrary moment order. We test our second-order Gaussian approximation (SOGA) on a number of case studies from the literature. We show that it can provide accurate estimates in models not supported by other approximation methods or when exact symbolic techniques fail because of complex expressions or non-simplified integrals. On two notable classes of problems, namely collaborative filtering and programs involving mixtures of continuous and discrete distributions, we show that SOGA significantly outperforms alternative techniques in terms of accuracy and computational time. Francesca Randone, Luca Bortolussi, Emilio Incerto, Mirco Tribastone |
Proc. ACM Program. Lang. | 2 |
| 2023 | Conformal Quantitative Predictive Monitoring of STL Requirements for Stochastic ProcessesabstractWe consider the problem of predictive monitoring (PM), i.e., predicting at runtime the satisfaction of a desired property from the current system’s state. Due to its relevance for runtime safety assurance and online control, PM methods need to be efficient to enable timely interventions against predicted violations, while providing correctness guarantees. We introduce quantitative predictive monitoring (QPM), the first PM method to support stochastic processes and rich specifications given in Signal Temporal Logic (STL). Unlike most of the existing PM techniques that predict whether or not some property ϕ is satisfied, QPM provides a quantitative measure of satisfaction by predicting the quantitative (aka robust) STL semantics of ϕ. QPM derives prediction intervals that are highly efficient to compute and with probabilistic guarantees, in that the intervals cover with arbitrary probability the STL robustness values relative to the stochastic evolution of the system. To do so, we take a machine-learning approach and leverage recent advances in conformal inference for quantile regression, thereby avoiding expensive Monte Carlo simulations at runtime to estimate the intervals. We also show how our monitors can be combined in a compositional manner to handle composite formulas, without retraining the predictors or sacrificing the guarantees. We demonstrate the effectiveness and scalability of QPM over a benchmark of four discrete-time stochastic processes with varying degrees of complexity. Francesca Cairoli, Nicola Paoletti, Luca Bortolussi |
HSCC | 3 |
| 2023 | Scalable Stochastic Parametric Verification with Stochastic Variational Smoothed Model Checking
Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, Paolo Pulcini |
RV | 1 |
| 2023 | Learning-Based Approaches to Predictive Monitoring with Conformal Statistical Guarantees
Francesca Cairoli, Luca Bortolussi, Nicola Paoletti |
RV | 2 |
| 2023 | MoonLight: a lightweight tool for monitoring spatio-temporal propertiesabstractAbstract We present MoonLight, a tool for monitoring temporal and spatio-temporal properties of mobile, spatially distributed, and interacting entities such as biological and cyber-physical systems. In MoonLight the space is represented as a weighted graph describing the topological configuration in which the single entities are arranged. Both nodes and edges have attributes modeling physical quantities and logical states of the system evolving in time. MoonLight is implemented in Java and supports the monitoring of Spatio-Temporal Reach and Escape Logic (STREL). MoonLight can be used as a standalone command line tool, such as Java API, or via Matlab™ and Python interfaces. We provide here the description of the tool, its interfaces, and its scripting language using a sensor network and a bike sharing example. We evaluate the tool performances both by comparing it with other tools specialized in monitoring only temporal properties and by monitoring spatio-temporal requirements considering different sizes of dynamical and spatial graphs. Laura Nenzi, Ezio Bartocci, Luca Bortolussi, Simone Silvetti, Michele Loreti |
Int. J. Softw. Tools Technol. Transf. | 3 |
| 2023 | Generative abstraction of Markov population processes
Francesca Cairoli, Fabio Anselmi, Alberto d'Onofrio, Luca Bortolussi |
Theor. Comput. Sci. | 4 |
| 2022 | Resilience of Bayesian Layer-Wise Explanations under Adversarial AttacksabstractWe consider the problem of the stability of saliency-based explanations of Neural Network predictions under adversarial attacks in a classification task. Saliency interpretations of deterministic Neural Networks are remarkably brittle even when the attacks fail, i.e. for attacks that do not change the classification label. We empirically show that interpretations provided by Bayesian Neural Networks are considerably more stable under adversarial perturbations of the inputs and even under direct attacks to the explanations. By leveraging recent results, we also provide a theoretical explanation of this result in terms of the geometry of the data manifold. Additionally, we discuss the stability of the interpretations of high level representations of the inputs in the internal layers of a Network. Our results demonstrate that Bayesian methods, in addition to being more robust to adversarial attacks, have the potential to provide more stable and interpretable assessments of Neural Network predictions. Ginevra Carbone, Luca Bortolussi, Guido Sanguinetti |
IJCNN | 2 |
| 2022 | Neural Predictive Monitoring for Collective Adaptive Systems
Francesca Cairoli, Nicola Paoletti, Luca Bortolussi |
ISoLA (3) | 3 |
| 2022 | Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic ProcessesabstractAbstract We introduce a similarity function on formulae of signal temporal logic (STL). It comes in the form of akernel function, well known in machine learning as a conceptually and computationally efficient tool. The correspondingkernel trickallows us to circumvent the complicated process of feature extraction, i.e. the (typically manual) effort to identify the decisive properties of formulae so that learning can be applied. We demonstrate this consequence and its advantages on the task ofpredicting (quantitative) satisfactionof STL formulae on stochastic processes: Using our kernel and the kernel trick, we learn (i) computationally efficiently (ii) a practically precise predictor of satisfaction, (iii) avoiding the difficult task of finding a way to explicitly turn formulae into vectors of numbers in a sensible way. We back the high precision we have achieved in the experiments by a theoretically sound PAC guarantee, ensuring our procedure efficiently delivers a close-to-optimal predictor. Luca Bortolussi, Giuseppe Maria Gallo, Jan Kretínský, Laura Nenzi |
TACAS (1) | 1 |
| 2022 | A Logic for Monitoring Dynamic Networks of Spatially-distributed Cyber-Physical SystemsabstractCyber-Physical Systems (CPS) consist of inter-wined computational (cyber) and physical components interacting through sensors and/or actuators. Computational elements are networked at every scale and can communicate with each other and with humans. Nodes can join and leave the network at any time or they can move to different spatial locations. In this scenario, monitoring spatial and temporal properties plays a key role in the understanding of how complex behaviors can emerge from local and dynamic interactions. We revisit here the Spatio-Temporal Reach and Escape Logic (STREL), a logic-based formal language designed to express and monitor spatio-temporal requirements over the execution of mobile and spatially distributed CPS. STREL considers the physical space in which CPS entities (nodes of the graph) are arranged as a weighted graph representing their dynamic topological configuration. Both nodes and edges include attributes modeling physical and logical quantities that can evolve over time. STREL combines the Signal Temporal Logic with two spatial modalities reach and escape that operate over the weighted graph. From these basic operators, we can derive other important spatial modalities such as everywhere, somewhere and surround. We propose both qualitative and quantitative semantics based on constraint semiring algebraic structure. We provide an offline monitoring algorithm for STREL and we show the feasibility of our approach with the application to two case studies: monitoring spatio-temporal requirements over a simulated mobile ad-hoc sensor network and a simulated epidemic spreading model for COVID19. Laura Nenzi, Ezio Bartocci, Luca Bortolussi, Michele Loreti |
Log. Methods Comput. Sci. | 3 |
| 2021 | Random Projections for Improved Adversarial RobustnessabstractWe propose two training techniques for improving the robustness of Neural Networks to adversarial attacks, i.e. manipulations of the inputs that are maliciously crafted to fool networks into incorrect predictions. Both methods are independent of the chosen attack and leverage random projections of the original inputs, with the purpose of exploiting both dimensionality reduction and some characteristic geometrical properties of adversarial perturbations. The first technique is called RP-Ensemble and consists of an ensemble of networks trained on multiple projected versions of the original inputs. The second one, named RP-Regularizer, adds instead a regularization term to the training objective. Ginevra Carbone, Guido Sanguinetti, Luca Bortolussi |
IJCNN | 3 |
| 2021 | Neural Predictive Monitoring Under Partial Observability
Francesca Cairoli, Luca Bortolussi, Nicola Paoletti |
RV | 2 |
| 2021 | Analysis of Markov Jump Processes under Terminal ConstraintsabstractAbstract Many probabilistic inference problems such as stochastic filtering or the computation of rare event probabilities require model analysis under initial and terminal constraints. We propose a solution to thisbridging problemfor the widely used class of population-structured Markov jump processes. The method is based on a state-space lumping scheme that aggregates states in a grid structure. The resulting approximate bridging distribution is used to iteratively refine relevant and truncate irrelevant parts of the state-space. This way, the algorithm learns a well-justified finite-state projection yielding guaranteed lower bounds for the system behavior under endpoint constraints. We demonstrate the method’s applicability to a wide range of problems such as Bayesian inference and the analysis of rare events. Michael Backenköhler, Luca Bortolussi, Gerrit Grossmann, Verena Wolf 0001 |
TACAS (1) | 2 |
| 2021 | Neural predictive monitoring and a comparison of frequentist and Bayesian approachesabstractAbstract Neural state classification (NSC) is a recently proposed method for runtime predictive monitoring of hybrid automata (HA) using deep neural networks (DNNs). NSC trains a DNN as an approximate reachability predictor that labels an HA state x as positive if an unsafe state is reachable from x within a given time bound, and labels x as negative otherwise. NSC predictors have very high accuracy, yet are prone to prediction errors that can negatively impact reliability. To overcome this limitation, we present neural predictive monitoring (NPM), a technique that complements NSC predictions with estimates of the predictive uncertainty. These measures yield principled criteria for the rejection of predictions likely to be incorrect, without knowing the true reachability values. We also present an active learning method that significantly reduces the NSC predictor’s error rate and the percentage of rejected predictions. We develop two versions of NPM based, respectively, on the use of frequentist and Bayesian techniques to learn the predictor and the rejection rule. Both versions are highly efficient, with computation times on the order of milliseconds, and effective, managing in our experimental evaluation to successfully reject almost all incorrect predictions. In our experiments on a benchmark suite of six hybrid systems, we found that the frequentist approach consistently outperforms the Bayesian one. We also observed that the Bayesian approach is less practical, requiring a careful and problem-specific choice of hyperparameters. Luca Bortolussi, Francesca Cairoli, Nicola Paoletti, Scott A. Smolka, Scott D. Stoller |
Int. J. Softw. Tools Technol. Transf. | 1 |
| 2020 | Robustness of Bayesian Neural Networks to Gradient-Based AttacksabstractVulnerability to adversarial attacks is one of the principal hurdles to the adoption of deep learning in safety-critical applications. Despite significant efforts, both practical and theoretical, the problem remains open. In this paper, we analyse the geometry of adversarial attacks in the large-data, overparametrized limit for Bayesian Neural Networks (BNNs). We show that, in the limit, vulnerability to gradient-based attacks arises as a result of degeneracy in the data distribution, i.e., when the data lies on a lower-dimensional submanifold of the ambient space. As a direct consequence, we demonstrate that in the limit BNN posteriors are robust to gradient-based adversarial attacks. Experimental results on the MNIST and Fashion MNIST datasets with BNNs trained with Hamiltonian Monte Carlo and Variational Inference support this line of argument, showing that BNNs can display both high accuracy and robustness to gradient based adversarial attacks. Ginevra Carbone, Matthew Wicker, Luca Laurenti, Andrea Patanè, Luca Bortolussi, Guido Sanguinetti |
NeurIPS | 5 |
| 2020 | MoonLight: A Lightweight Tool for Monitoring Spatio-Temporal Properties
Ezio Bartocci, Luca Bortolussi, Michele Loreti, Laura Nenzi, Simone Silvetti |
RV | 2 |
| 2020 | Monitoring Spatio-Temporal Properties (Invited Tutorial)
Laura Nenzi, Ezio Bartocci, Luca Bortolussi, Michele Loreti, Ennio Visconti |
RV | 3 |
| 2020 | Fluid approximation of broadcasting systems
Luca Bortolussi, Jane Hillston, Michele Loreti |
Theor. Comput. Sci. | 1 |
| 2019 | Neural Predictive Monitoring
Luca Bortolussi, Francesca Cairoli, Nicola Paoletti, Scott A. Smolka, Scott D. Stoller |
RV | 1 |
| 2019 | Size expansions of mean field approximation: Transient and steady-state analysis
Nicolas Gast, Luca Bortolussi, Mirco Tribastone |
Perform. Evaluation | 2 |
| 2019 | Central Limit Model CheckingabstractWe consider probabilistic model checking for continuous-time Markov chains (CTMCs) induced from Stochastic Reaction Networks against a fragment of Continuous Stochastic Logic (CSL) extended with reward operators. Classical numerical algorithms for CSL model checking based on uniformisation are limited to finite CTMCs and suffer from exponential growth of the state space with respect to the number of species. However, approximate techniques such as mean-field approximations and simulations combined with statistical inference are more scalable but can be time-consuming and do not support the full expressiveness of CSL. In this article, we employ a continuous-space approximation of the CTMC in terms of a Gaussian process based on the Central Limit Approximation, also known as the Linear Noise Approximation, whose solution requires solving a number of differential equations that is quadratic in the number of species and independent of the population size. We then develop efficient and scalable approximate model checking algorithms on the resulting Gaussian process, where we restrict the target regions for probabilistic reachability to convex polytopes. This allows us to derive an abstraction in terms of a time-inhomogeneous discrete-time Markov chain (DTMC), whose dimension is independent of the number of species, on which model checking is performed. Using results from probability theory, we prove the convergence in distribution of our algorithms to the corresponding measures on the original CTMC. We implement the techniques and, on a set of examples, demonstrate that they allow us to overcome the state space explosion problem, while still correctly characterizing the stochastic behaviour of the system. Our methods can be used for formal analysis of a wide range of distributed stochastic systems, including biochemical systems, sensor networks, and population protocols. Luca Bortolussi, Luca Cardelli, Marta Z. Kwiatkowska, Luca Laurenti |
ACM Trans. Comput. Log. | 1 |
| 2018 | Signal Convolution Logic
Simone Silvetti, Laura Nenzi, Ezio Bartocci, Luca Bortolussi |
ATVA | 4 |
| 2018 | Bayesian Statistical Parameter Synthesis for Linear Temporal Properties of Stochastic Models
Luca Bortolussi, Simone Silvetti |
TACAS (2) | 1 |
| 2018 | Model checking Markov population models by stochastic approximations
Luca Bortolussi, Roberta Lanciani, Laura Nenzi |
Inf. Comput. | 1 |
| 2018 | Qualitative and Quantitative Monitoring of Spatio-Temporal Properties with SSTLabstractIn spatially located, large scale systems, time and space dynamics interact and drives the behaviour. Examples of such systems can be found in many smart city applications and Cyber-Physical Systems. In this paper we present the Signal Spatio-Temporal Logic (SSTL), a modal logic that can be used to specify spatio-temporal properties of linear time and discrete space models. The logic is equipped with a Boolean and a quantitative semantics for which efficient monitoring algorithms have been developed. As such, it is suitable for real-time verification of both white box and black box complex systems. These algorithms can also be combined with stochastic model checking routines. SSTL combines the until temporal modality with two spatial modalities, one expressing that something is true somewhere nearby and the other capturing the notion of being surrounded by a region that satisfies a given spatio-temporal property. The monitoring algorithms are implemented in an open source Java tool. We illustrate the use of SSTL analysing the formation of patterns in a Turing Reaction-Diffusion system and spatio-temporal aspects of a large bike-sharing system. Comment: 36 pages with 13 figures Laura Nenzi, Luca Bortolussi, Vincenzo Ciancia, Michele Loreti, Mieke Massink |
Log. Methods Comput. Sci. | 2 |
| 2018 | Moment-Based Parameter Estimation for Stochastic Reaction Networks in EquilibriumabstractCalibrating parameters is a crucial problem within quantitative modeling approaches to reaction networks. Existing methods for stochastic models rely either on statistical sampling or can only be applied to small systems. Here, we present an inference procedure for stochastic models in equilibrium that is based on a moment matching scheme with optimal weighting and that can be used with high-throughput data like the one collected by flow cytometry. Our method does not require an approximation of the underlying equilibrium probability distribution and, if reaction rate constants have to be learned, the optimal values can be computed by solving a linear system of equations. We discuss important practical issues such as the selection of the moments and evaluate the effectiveness of the proposed approach on three case studies. Michael Backenköhler, Luca Bortolussi, Verena Wolf 0001 |
IEEE ACM Trans. Comput. Biol. Bioinform. | 2 |
| 2017 | Reachability Computation for Switching Diffusions: Finite Abstractions with Certifiable and Tuneable PrecisionabstractWe consider continuous time stochastic hybrid systems with no resets and continuous dynamics described by linear stochastic differential equations -- models also known as switching diffusions. We show that for this class of models reachability (and dually, safety) properties can be studied on an abstraction defined in terms of a discrete time and finite space Markov chain (DTMC), with provable error bounds. The technical contribution of the paper is a characterization of the uniform convergence of the time discretization of such stochastic processes with respect to safety properties. This allows us to newly provide a complete and sound numerical procedure for reachability and safety computation over switching diffusions. Luca Laurenti, Alessandro Abate, Luca Bortolussi, Luca Cardelli, Milan Ceska 0002, Marta Z. Kwiatkowska |
HSCC | 3 |
| 2017 | An Active Learning Approach to the Falsification of Black Box Cyber-Physical Systems
Simone Silvetti, Alberto Policriti, Luca Bortolussi |
IFM | 3 |
| 2017 | Monitoring mobile and spatially distributed cyber-physical systemsabstractCyber-Physical Systems (CPS) consist of collaborative, networked and tightly intertwined computational (logical) and physical components, each operating at different spatial and temporal scales. Hence, the spatial and temporal requirements play an essential role for their correct and safe execution. Furthermore, the local interactions among the system components result in global spatio-temporal emergent behaviors often impossible to predict at the design time. In this work, we pursue a complementary approach by introducing STREL a novel spatio-temporal logic that enables the specification of spatio-temporal requirements and their monitoring over the execution of mobile and spatially distributed CPS. Our logic extends the Signal Temporal Logic [15]with two novel spatial operators reach and escape from which is possible to derive other spatial modalities such as everywhere, somewhere and surround. These operators enable a monitoring procedure where the satisfaction of the property at each location depends only on the satisfaction of its neighbours, opening the way to future distributed online monitoring algorithms. We propose both a qualitative and quantitative semantics based on constraint semirings, an algebraic structure suitable for constraint satisfaction and optimisation. We prove that, for a subclass of models, all the spatial properties expressed with reach and escape, using euclidean distance, satisfy all the model transformations using rotation, reflection and translation. Finally, we provide an offline monitoring algorithm for STREL and, to demonstrate the feasibility of our approach, we show its application using the monitoring of a simulated mobile ad-hoc sensor network as running example. Ezio Bartocci, Luca Bortolussi, Michele Loreti, Laura Nenzi |
MEMOCODE | 2 |
| 2017 | Policy learning in continuous-time Markov decision processes using Gaussian Processes
Ezio Bartocci, Luca Bortolussi, Tomás Brázdil, Dimitrios Milios, Guido Sanguinetti |
Perform. Evaluation | 2 |
| 2016 | Mean Field Approximation of Uncertain Stochastic ModelsabstractWe consider stochastic models in presence of uncertainty, originating from lack of knowledge of parameters or by unpredictable effects of the environment. We focus on population processes, encompassing a large class of systems, from queueing networks to epidemic spreading. We set up a formal framework for imprecise stochastic processes, where some parameters are allowed to vary in time within a given domain, but with no further constraint. We then consider the limit behaviour of these systems as the population size goes to infinity. We prove that this limit is given by a differential inclusion that can be constructed from the (imprecise) drift. We provide results both for the transient and the steady state behaviour. Finally, we discuss different approaches to compute bounds of the so-obtained differential inclusions, proposing an effective control-theoretic method based on Pontryagin principle for transient bounds. This provides an efficient approach for the analysis and design of large-scale uncertain and imprecise stochastic models. The theoretical results are accompanied by an in-depth analysis of an epidemic model and a queueing network. These examples demonstrate the applicability of the numerical methods and the tightness of the approximation. Luca Bortolussi, Nicolas Gast |
DSN | 1 |
| 2016 | Hybrid behaviour of Markov population models
Luca Bortolussi |
Inf. Comput. | 1 |
| 2016 | Smoothed model checking for uncertain Continuous-Time Markov Chains
Luca Bortolussi, Dimitrios Milios, Guido Sanguinetti |
Inf. Comput. | 1 |
| 2016 | Editorial: Quantitative Aspects of Programming Languages and Systems
Nathalie Bertrand 0001, Luca Bortolussi, Herbert Wiklicky |
Theor. Comput. Sci. | 2 |
| 2015 | Machine Learning Methods in Statistical Model Checking and System Design - Tutorial
Luca Bortolussi, Dimitrios Milios, Guido Sanguinetti |
RV | 1 |
| 2015 | Qualitative and Quantitative Monitoring of Spatio-Temporal Properties
Laura Nenzi, Luca Bortolussi, Vincenzo Ciancia, Michele Loreti, Mieke Massink |
RV | 2 |
| 2015 | Coding Theory: A General Framework and Two Inverse ProblemsabstractWe put forward an ample framework for coding based on upper probabilities, or more generally on normalized monotone set-measures, and model accordingly noisy transmission channels and decoding errors. Two inverse problems are considered. In the first case, a decoder is given and one looks for chann els of a specified family over which that decoder would work properly. In the second and more ambitious case, it is codes which are given, and one looks for channels over which those codes would ensure the required error correction capabilities. Upper probabilities allow for a solution of the two inverse problems in the case of usual codes based on checking Hamming distances between codewords: one can equivalently check suitable upper probabilities of the decoding errors. This soon extends to “odd” codeword distances for DNA strings as used in DNA word design, where instead, as we prove, not even the first unassuming inverse problem admits of a solution if one insists on channel models based on “usual” probabilities. Luca Bortolussi, Liviu P. Dinu, Laura Franzoi, Andrea Sgarro |
Fundam. Informaticae | 1 |
| 2015 | Model checking single agent behaviours by fluid approximation
Luca Bortolussi, Jane Hillston |
Inf. Comput. | 1 |
| 2015 | System design of stochastic models using robustness of temporal properties
Ezio Bartocci, Luca Bortolussi, Laura Nenzi, Guido Sanguinetti |
Theor. Comput. Sci. | 2 |
| 2014 | Temporal Logic Based Monitoring of Assisted Ventilation in Intensive Care Patients
Sara Bufo, Ezio Bartocci, Guido Sanguinetti, Massimo Borelli, Umberto Lucangelo, Luca Bortolussi |
ISoLA (2) | 6 |
| 2014 | Hybrid Systems and Biology
Ezio Bartocci, Luca Bortolussi, Scott A. Smolka |
Inf. Comput. | 2 |
| 2013 | Stochastic Process Algebra and Stability Analysis of Collective Systems
Luca Bortolussi, Diego Latella, Mieke Massink |
COORDINATION | 1 |
| 2013 | HYPE: Hybrid modelling by composition of flowsabstractAbstract Hybrid systems are manifest in both the natural and the engineered world, and their complex nature, mixing discrete control and continuous evolution, make it difficult to predict their behaviour. In recent years several process algebras for modelling hybrid systems have appeared in the literature, aimed at addressing this problem. These all assume that continuous variables in the system are modelled monolithically, often with differential equations embedded explicitly in the syntax of the process algebra expression. In HYPE an alternative approach is taken which offers finer-grained modelling with each flow or influence affecting a variable modelled separately. The overall behaviour then emerges as the composition of flows. In this paper we give a detailed account of the HYPE process algebra, its semantics, and its use for verification of systems. We establish both syntactic conditions (well-definedness) and operational restrictions (well-behavedness) to ensure reasonable behaviour in HYPE models. Furthermore we consider how the equivalence relation defined for HYPE relates to other relations previously proposed in the literature, demonstrating that our fine-grained approach leads to a more discriminating notion of equivalence. We present the HYPE model of a standard hybrid system example, both establishing that our approach can reproduce the previously obtained results and demonstrating how our compositional approach supports variations of the problem in a straightforward and flexible way. Vashti Galpin, Luca Bortolussi, Jane Hillston |
Formal Aspects Comput. | 2 |
| 2013 | (Hybrid) automata and (stochastic) programsThe hybrid automata lattice of a stochastic programabstractWe define a semantics for stochastic Concurrent Constraint Programming (sCCP), a stochastic process algebra, in terms of stochastic hybrid automata with piecewise deterministic continuous dynamics. To each program we associate a lattice of hybrid models, parameterized with respect to the degree of discreteness left. We study some properties of this lattice, presenting also an alternative semantics in which the degree of discreteness can be dynamically changed. Luca Bortolussi, Alberto Policriti |
J. Log. Comput. | 1 |
| 2013 | Bounds on the deviation of discrete-time Markov chains from their mean-field model
Luca Bortolussi, Richard A. Hayden |
Perform. Evaluation | 1 |
| 2013 | Continuous approximation of collective system behaviour: A tutorial
Luca Bortolussi, Jane Hillston, Diego Latella, Mieke Massink |
Perform. Evaluation | 1 |
| 2012 | Fluid Model Checking
Luca Bortolussi, Jane Hillston |
CONCUR | 1 |
| 2012 | Fluid limit of an asynchronous optical packet switch with shared per link full range wavelength conversionabstractWe consider an asynchronous all optical packet switch (OPS) where each link consists of N wavelength channels and a pool of C ≤ N full range tunable wavelength converters. Under the assumption of Poisson arrivals with rate λ (per wavelength channel) and exponential packet lengths, we determine a simple closed-form expression for the limit of the loss probabilities Ploss(N) as N tends to infinity (while the load and conversion ratio σ=C/N remains fixed). More specifically, for σ ≤ λ2 the loss probability tends to (λ2-σ)/λ(1+λ), while for σ > λ2 the loss tends to zero. We also prove an insensitivity result when the exponential packet lengths are replaced by certain classes of phase-type distributions. A key feature of the dynamical system (i.e., set of ODEs) that describes the limit behavior of this OPS switch, is that its right-hand side is discontinuous. To prove the convergence, we therefore had to generalize some existing result to the setting of piece-wise smooth dynamical systems. Benny Van Houdt, Luca Bortolussi |
SIGMETRICS | 2 |
| 2012 | Fluid limits of queueing networks with batchesabstractThis paper presents an analytical model for the performance prediction of queueing networks with batch services and batch arrivals, related to the fluid limit of a suitable single-parameter sequence of continuous-time Markov chains and interpreted as the deterministic approximation of the average behaviour of the stochastic process. Notably, the underlying system of ordinary differential equations exhibits discontinuities in the right-hand sides, which however are proven to yield a meaningful solution. A substantial numerical assessment is used to study the quality of the approximation and shows very good accuracy in networks with large job populations. Luca Bortolussi, Mirco Tribastone |
ICPE | 1 |
| 2012 | Spearman Permutation Distances and Shannon's DistinguishabilityabstractSpearman distance is a permutation distance which might be used for codes in permutations beside Kendall distance. However, Spearman distance gives rise to a geometry of strings, which is rather unruly from the point of view of error correction and error detection. Special care has to be taken to discriminate between the two notions of codeword distance and codeword distinguishability. This stresses the importance of rejuvenating the latter notion, extending it from Shannon's zero-error information theory to the more general setting of metric string distances. Luca Bortolussi, Liviu P. Dinu, Andrea Sgarro |
Fundam. Informaticae | 1 |
| 2010 | Hybrid dynamics of stochastic programs
Luca Bortolussi, Alberto Policriti |
Theor. Comput. Sci. | 1 |
| 2009 | Stochastic Programs and Hybrid Automata for (Biological) Modeling
Luca Bortolussi, Alberto Policriti |
CiE | 1 |
| 2009 | HYPE: A Process Algebra for Compositional Flows and Emergent Behaviour
Vashti Galpin, Luca Bortolussi, Jane Hillston |
CONCUR | 2 |
| 2007 | Constraint-Based Simulation of Biological Systems Described by Molecular Interaction MapsabstractWe present a method to simulate biochemical networks described by the graphical notation of Molecular Interaction Maps within stochastic Concurrent Constraint Programming. Such maps are compact, as they represent implicitly a wide set of reactions, and therefore not easy to simulate with standard tools. The encoding we propose is capable to stochastically simulate these maps implicitly, without generating the full list of reactions. Luca Bortolussi, Simone Fonda, Alberto Policriti |
BIBM | 1 |
| 2005 | Concurrent Methodologies for Global Optimization
Luca Bortolussi |
ICLP | 1 |
| 2005 | A Distributed and Probabilistic Concurrent Constraint Programming Language
Luca Bortolussi, Herbert Wiklicky |
ICLP | 1 |
| 2004 | Fuzzy Possibilities As Upper PrevisionsabstractIn this paper we analyze, mainly in a finitary setting, the consistency properties of fuzzy possibilities, interpreting them as instances of upper previsions and applying the basic notions of avoiding sure loss and coherence from the theory of imprecise probabilities. It ensues that fuzzy possibilities always avoid sure loss, but satisfy the stronger coherence condition only in a special case. Their natural extension, i.e. their least-committal correction to a coherent upper prevision, is determined. The same analysis is then performed when min is replaced in the definition of fuzzy possibility by a T–norm or, more generally, a seminorm, showing that the consistency properties and also the natural extension remain the same. Some "closure" properties are also discussed, which are guaranteed to hold if the T–seminorm is continuous, and are satisfied by (ordinary) possibilities too. Paolo Vicig, Luca Bortolussi |
Int. J. Uncertain. Fuzziness Knowl. Based Syst. | 2 |