Our paper "P³MC: Towards Probabilistic Programming-Based Model Checking for Linear Temporal Logic", by Luca Bortolussi, Romina Doz, Laura Nenzi, Francesca Randone, Simone Silvetti and Mirco Tribastone was accepted at ISOLA 2026 in the Rigorous Engineering of Collective Adaptive Systems track!
A fundamental challenge in the analysis of stochastic systems is verifying whether they satisfy temporal properties — for instance, whether a physical process eventually reaches a target region, or remains stable over time. Traditional model checking tools handle this well for discrete systems, but struggle when continuous random variables are involved.
In this paper, we propose a new approach that encodes stochastic dynamical systems as probabilistic programs and leverages their analytical Gaussian Mixture semantics (computed by DEGAS) to estimate — and optimize — the probability that a given temporal property is satisfied, without any Monte Carlo sampling.
Our initial evaluation on on three systems with qualitatively different dynamics shows that both methods can accurately estimate satisfaction probabilities and optimize system parameters to maximize them.
A promising start for bridging model checking of continuous systems and probabilistic programming!
📖 Pre-print soon available
Our paper "Inferring Structural Causal Models from Data with Grammatical Evolution", by Romina Doz, Francesca Randone, Luca Bortolussi and Eric Medvet was accepted at PPSN 2026!
Understanding cause-and-effect relationships in complex systems is a fundamental challenge in science. While traditional statistics can reveal correlations, causal models go a step further by explicitly mapping how one variable causes another, and not just correlates to it.
In this paper, we tackle the following problem: can we automatically learn causal structures directly from data, without prior knowledge of the underlying system? Our approach couples evolutionary computation in the form of Grammatical Evolution (an algorithm able to generate programs mimicking natural selection) and probabilistic programming to represent causal models in a suitable form.
We show that the approach is able to recover simple causal structures that then combine to form complex models.
📖 Pre-print available at: https://medvet.inginf.units.it/publications/2026-c-drbm-inferring/
👾 Implementation available at: https://github.com/r-doz/Causal_Models_Synthesis
As part of the joint FORSYTE/ISTA seminar series I held a seminar titled "Probabilistic Programming: Semantics and Statistical Perspectives".
Our paper "DeGAS: Gradient-Based Optimization of Probabilistic Programs without Sampling", by Francesca Randone, Romina Doz, Mirco Tribastone and Luca Bortolussi was accepted at TACAS 2026!
Remember SOGA, our PPL to enable inference of probabilistic programs with continuous and discrete variables?
DeGAS is its evolution, aimed at solving complex optimization problems.
DeGAS augments SOGA syntax with parameters, and applies a semantic smoothing to ensure that the posterior is always differentiable, even in presence of discrete random variables. By doing that, it allows you to optimize the parameters using torch gradient-based optimization. We have used DeGAS to optimize parameters in CPS models observing very nice results. In particular, we were able to optimize complex loss functions, not just standard likelihoods.
📖 Pre-print available at: https://arxiv.org/pdf/2601.15167
📦 Replication package available at: https://zenodo.org/records/18197807
👾 DeGAS available at: https://github.com/frarandone/DeGAS (repo under active development)