Auditorium (Building IMAG)
19 septembre 2019 - 14h00
What’s to Come is Still Unsure: Automatically Synthesizing and Verifying Controllers Resilient to Delayed Interaction
par Martin Franzle de Carl von Ossietzky Universitat Oldenburg, Germany
Abstract: The advent of systems of cooperative cyber-physical systems draws
attention to a central problem of networked and distributed control
systems: the ubiquity of delay in feedback loops between logically or
spatially distributed components, which is not adequately reflected in
traditional models of hybrid-state dynamics based on ordinary differential
equations and immediate transitions. Occurrence of feedback delays may
significantly alter a system's dynamic response. Unmodeled delays in a
control loop consequently have the potential to invalidate any stability
and safety certificate obtained on a related delay-free model, which is
current practice in hybrid-system analysis. In this talk, we will present
various approaches to the analysis and correct-by-construction design of
dynamical systems subject to delayed information exchange, as pertinent to
distributed hybrid systems. We will explain automatic verification
procedures for invariance properties and bounded temporal-logic based on
constraint-solving or rigorous generalization from simulations. This
analytical view will be complemented by a constructive one based on a
notion of delayed games and corresponding strategy synthesis algorithms.
(joint work with Erzana Berani Abdelwahab, Mingshuai Chen, Yangjia Li, Peter Nazier Mosaad, and Naijun Zhan)
CV: Martin Franzle is Professor for Hybrid Discrete-Continuous Systems at
the Carl von Ossietzky Universitat Oldenburg, Germany. Previous positions
include an associate professorship and a Velux visiting professorship at
the Technical University of Denmark, post-doctoral position at Oldenburg
and Kiel, a doctoral researcher position at Kiel, where he also
obtained his doctoral degree. His research interests are in modelling,
verification, and synthesis of reactive, real-time, and hybrid dynamics in
embedded and cyber-physical systems. He has worked on the semantics of
high-level modelling and specification languages and on decision problems
and their application to verifying and synthesizing real-time and hybrid
discrete-continuous systems including settings subject to stochastic
disturbances.
