What’s to Come is Still Unsure: Automatically Synthesizing and Verifying Controllers Resilient to Delayed Interaction

Martin Fränzle
Friday, 22 February, 2019 - 09:45
NO-5, Solvay Room

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