Autonomy Talks - Abolfazl Lavaei: Automated Verification and Control of Large-​Scale Stochastic CPSs

Autonomy Talks - 23/12/2020

Speaker: Dr. Abolfazl Lavaei, Institute for Dynamic Systems and Control, ETH Zürich

Title: Automated Verification and Control of Large-Scale Stochastic Cyber-Physical Systems: Compositional Techniques

Abstract: In the past few years, stochastic cyber-physical systems (CPSs) have received remarkable attentions as an important modeling framework describing many engineering systems, and play significant roles in different real-life applications including traffic networks, trans- portation systems, power grids, and so on. Automated verification and policy synthesis for this type of complex stochastic systems to achieve some high-level specifications, e.g., those expressed as linear temporal logic (LTL) formulae, are inherently very challeng- ing. In particular, the ability to handle the interaction between continuous and discrete dynamics in CPSs is a prerequisite to provide a rigorous formal framework for the auto- mated verification and synthesis of those complex systems. Since the complexity induced by the aforementioned interaction often makes it difficult to obtain analytical results, one promising solution is to first employ (in)finite abstractions of systems as replacements of original (concrete) ones, then synthesize discrete controllers for abstract systems, and finally refine controllers back to concrete models via a hybrid interface map. Since the mismatch between the output of the concrete system and that of its abstraction is well- quantified, one can guarantee that the concrete system also satisfies the same property as the abstract one with guaranteed error bounds on their output trajectories. Unfortu- nately, construction of abstractions for large-scale CPSs in a monolithic manner suffers severely from the so-called curse of dimensionality: the complexity grows exponentially as the number of state variables increases. In this talk, I will present different scalable com- positional techniques to analyze and control large-scale stochastic CPSs in an automated as well as formal fashion.

Find out more at https://idsc.ethz.ch/research-frazzoli/autonomy-talks.html

Видео Autonomy Talks - Abolfazl Lavaei: Automated Verification and Control of Large-​Scale Stochastic CPSs канала Autonomy Talks