Computational and simulation-based science and engineering are undergoing a revolution due to the advent of artificial intelligence and machine learning techniques. The combination of simulation based approaches with machine learning gave rise to the new field of simulation intelligence. Reinforcement learning, in addition, is revolutionising traditional control and automation approaches and game and decision theory.
In this rapidly evolving area, we work at the intersection between formal methods, control theory, cyber-physical systems, and artificial intelligence. We focus on autonomous Cyber-Physical Systems and leverage formal specification languages (Signal Temporal Logic) to either design them to be safe (Safe Reinforcement Learning) or to preemptively monitor their safety (Predictive Monitoring). We further explore surrogate models for discrete stochastic systems based on generative deep learning. As complexity increases, we move towards probabilistic reasoning to handle uncertainty and intrinsic stochasticity. We also explore the application of reinforcement learning to combinatorial optimisation problems.
Keywords: parametric verification, predictive monitoring, learning model abstractions, multi-agent Reinforcement Learning, Reinforcement Learning with memory, analysis of multimodal stock systems, networks, mean-field approximation of stochastic models.
In the following, there is a reasoned bibliography, in which each class of contributions is briefly described and the relevant bibliography is cited.
Smoothed Model Checking
Smoothed Model Checking is a parametric verification engine based on simulation and machine learning, for stochastic processes like Continuous Time Markov Chains. It leverages the power of Bayesian ML to infer the satisfaction probability as a function of model parameters and estimate the uncertainty of the predictions, that can be further used in an active learning refinement cycle. It has been used for parameter synthesis. Originally implemented using Gaussian Processes, it has been recently scaled up using stochastic variational inference.
- Bortolussi, Luca; Milios, Dimitrios; Sanguinetti, Guido. Smoothed model checking for uncertain continuous-time Markov chains. In: Information and Computation, vol. 247, pp. 235–253, 2016. Link
- Bortolussi, Luca; Silvetti, Simone. Bayesian statistical parameter synthesis for linear temporal properties of stochastic models. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 396–413, Springer, Cham 2018. Link
- Bortolussi, Luca; Cairoli, Francesca; Carbone, Ginevra; Pulcini, Paolo Scalable Stochastic Parametric Verification with Stochastic Variational Smoothed Model Checking. In: arXiv preprint arXiv:2205.05398, 2022. Link