Events Calendar

CS Colloquium: Simone Silvetti and Laura Nenzi

Speaker: Simone Silvetti (Numerical Methods Group) and Laura Nenzi (TU Wien),

Talk Title: Talk1: Combining Active learning optimization and Temporal logic for parameter synthesis and falsification of Complex Systems Talk 2: System Design of Stochastic Models using Robustness of Temporal Properties

Series: Computer Science Colloquium jointly with CCI-MHI Cyber-Physical Systems Seminar

Abstract: We are pleased to announce two talks during this colloquium.

Talk 1: Combining Active learning optimization and Temporal logic for parameter synthesis and falsification of Complex Systems
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.

Talk 2: System Design of Stochastic Models using Robustness of Temporal Properties
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.

This lecture satisfies requirements for CSCI 591: Research Colloquium. Please note, due to limited capacity in OHE 100D, seats will be first come first serve.


Biography: Talk 1: 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: 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.


Host: Jyotirmoy Deshmukh and Paul Bogdan

Location: Olin Hall of Engineering (OHE) - 100D

Audiences: Everyone Is Invited

Contact: Computer Science Department