Invited Speakers

 

Thao Dang - CNRS (French National Center for Scientific Research) and VERIMAG, Université Grenoble Alpes

Thao Dang obtained her Diplôme d'Ingénieur and PhD from the INPG (Institut National Polytechnique de Grenoble) in 1997 and 2000. In 2001 she was a postdoctoral researcher at University of Pennsylvania in Philadelphia. In 2002 she became a researcher at the CNRS (French National Center for Scientific Research) and then a CNRS Research Director (directrice de recherche) in 2014. She is also a permanent member of the VERIMAG laboratory, Université Grenoble Alpes. Her domains of expertise include hybrid systems formal verification and test generation, applications to Cyber-Physical Systems and Systems Biology. Her recent research is Cyber-Physical Systems integrating Artificial Intelligence and she is currently the principal investigator of a number of national and international projects on the topic.

Title:

A Behaviour-based Approach to Quantitative Validation of Cyber-Physical 
Systems

Abstract In this talk we describe a behaviour-based approach to quantitative  property validation of Cyber-Physical Systems (CPS). The heterogeneity and complexity of industrial CPS make a behaviour-based approach very desirable since It is widely recognized that it is hard or impossible to derive sound mathematical models for such systems. Quantitative validation means providing, instead of a Boolean answer about property satisfaction, quality measures, such as confidence interval, robustness bound, coverage of the set of tested behaviours over the set of all possible behaviours, etc.

We first discuss the problem of encoding and measuring CPS signal spaces with respect to some approximation quality measures. In particular, we consider signal spaces subject to temporal constraints, namely they must satisfy given timing assumptions or properties. For a set of (usually uncountably many) signals representing CPS behaviours of interest, an approximation quality measure reflects how well a finite set of signals sampled from the original set can replace the original set in terms of property validation. We discuss a number of measures for sets of temporal behaviours: uniformity, epsilon-entropy and discrepancy measures. We then describe methods for generating CPS signals with good approximation quality, by combining sampling (as in Monte Carlo and quasi-Monte Carlo methods) and optimisation. The approach is  finally illustrated on CPS benchmarks in particular in automative control.
 

Joël Ouaknine - Max Planck Institute for Software Systems

Joël Ouaknine is a Scientific Director at the Max Planck Institute for Software Systems in Saarbrücken, Germany. His research interests straddle theoretical computer science and mathematics, and lie mainly at the intersection of dynamical systems and computation, making use of tools from number theory, Diophantine geometry, algebraic geometry, and mathematical logic. Joël studied mathematics at McGill University, and received a PhD in Computer Science from Oxford in 2001. He subsequently held postdoc positions at Tulane University and Carnegie Mellon University, and became Full Professor of Computer Science at Oxford in 2010. He received the Roger Needham Award in 2010, an ERC grant in 2015, and was elected member of Academia Europaea in 2020; the same year he also received the Arto Salomaa Prize (jointly with James Worrell), for "outstanding contributions to Theoretical Computer Science, in particular to the theory of timed automata and to the analysis of dynamical systems". He was elected Fellow of the ACM in 2021 for "contributions to algorithmic analysis of dynamical systems".

Title

The Skolem Landscape

Abstract:

The Skolem Problem asks how to determine algorithmically whether a given  linear recurrence sequence (such as the Fibonacci numbers) has a zero. It is a central question in dynamical systems and number theory, and has many connections to other branches of mathematics and computer science, such as program analysis and the verification of dynamical, probabilistic, and hybrid systems. Unfortunately, the decidability of the Skolem Problem has been open for nearly a century! In this talk, I will present a survey of what is known on the Skolem Problem and related questions, including recent and ongoing developments.