CJoint Seminar about Systems with Computer Science Department

This is a joint seminar with the Computer Science Department

Talk #1: Combining Active learning optimization and Temporal logic for parameter synthesis and falsification of Complex Systems

ABSTRACT: In this talk, we discuss the combination of Active Learning Optimization and temporal logic to the falsification and parameter synthesis of complex dynamical systems. First, we introduce Gaussian Processes and an active learning approach aimed to falsify a black box model with time-dependent functional inputs. Second, we introduce a technique also base on Gaussian Processes, named Smoothed Model Checking, which is able to estimate the probability that a stochastic system satisfies a temporal logic formula. We leverage this estimation ability and an active learning approach to find regions of the parameter space where the model satisfies a temporal logic formula with probability greater (or less) than a given threshold.

BIO: Simone Silvetti is a researcher and developer at the Numerical Methods Group of Esteco SpA, Italy. He received a Ph.D. in Computer Science from the University of Udine in 2018 and a MSc in Mathematics from the University of Rome in 2012. His research focuses on the application of machine learning to quantitative formal methods and optimization.

Talk #2: System Design of Stochastic Models using Robustness of Temporal Properties

ABSTRACT: In the last years, researchers from the verification community have proposed several notions of robustness for temporal logic providing suitable definitions of distance between a trajectory of a (deterministic) dynamical system and the boundaries of the set of trajectories satisfying the property of interest. In this talk, we present an extension of this notion of robustness to stochastic systems, showing that this naturally leads to a distribution of robustness degrees. Then, we show how to exploit this notion to address the system design problem, where the goal is to optimise some control parameters of a stochastic model in order to maximise robustness of the desired specifications. The key idea is to use a learning algorithm to estimate the dependence of the average robustness of a qualitative formula over the model parameters. A powerful and provably convergent machine learning method, namely the Gaussian Process – Upper Confidence Bound (GP-UCB) algorithm is use to improve the parameter optimisation. Finally, we demonstrate the applicability of our method on a number of case studies and ongoing works.

BIO: Since 2017, Laura Nenzi is a research assistant at the TU Wien. She received a Ph.D in Computer Science from IMT Lucca, in 2016. In December 2018, she will join the University of Trieste as Assistant Professor. Her research interests include: spatio-temporal logics, statistical verification routines for uncertain models and combination of formal methods with machine learning techniques.

Hosted by: Paul Bogdan