Campus Event Calendar

Event Entry

What and Who

Formal Controller Synthesis for Dynamical Systems: Decidability and Scalability

Mahmoud Salamati
MMCI, CISPA Helmholtz Center for Information Security
SWS Student Defense Talks - Thesis Proposal
Public Audience

Date, Time and Location

Wednesday, 14 December 2022
60 Minutes


In cyber-physical systems research an important challenge is the synthesis of reliable controllers with respect to a general temporal specification. The synthesized controller must provide formal guarantees against different sources of uncertainty, such as measurement noise and mismatch between the dynamics of the physical system and its model, etc. By synthesizing correct-by-construction controllers for complex dynamical systems, we can enable a large number of exciting applications in various domains, including autonomous vehicle industry, energy systems and healthcare.

In this thesis, we plan to study controller synthesis for several different classes of dynamical systems. If it is not possible to give a complete and sound synthesis algorithm, we will try to propose a sound but scalable technique. Also, for some special classes of dynamics, we provide sound and complete decision procedures.

First, we consider continuous dynamical systems with bounded disturbance. The underlying dynamics for every continuous dynamical system can—in the bounded adversarial setting—be modeled by a (non-linear) differential inclusion system, provided that a bound over the range of model uncertainties is known. A common approach to tackle the continuous nature of the state space is to use abstraction-based controller design (ABCD) schemes. The controller designed by the ABCD scheme is described as being formal due to the guarantees on satisfaction of the specification by the original system in closed loop with the designed controller. In the first part of the thesis, we present methods to improve applicability of ABCD, by proposing (1) a data-driven scheme for relaxing the requirement of having analytical model, (2) a neural abstraction method to lower memory requirements of both synthesis and deployment, and (3) a scalable method for solving reach-avoid problems for multi-agent systems.

Second, we study continuous-time Markov decision processes (CTMDPs), which are a widely used model for continuous-time stochastic systems. A fundamental problem in the analysis of CTMDPs is time-bounded reachability, which asks whether we can synthesize a control policy with which the probability of reaching a target state within a finite horizon is greater than a given threshold. Time-bounded reachability is the core technical problem for model checking stochastic temporal logics such as Continuous Stochastic Logic, and having efficient implementations of time-bounded reachability is crucial to scaling formal analysis of CTMDPs. Existing work either considers time-abstract policies or focuses on numerical approximation. Despite the importance of this problem, its decidability is yet open. Moreover, the existing discretization-based approximation methods are not scalable for CTMDPs with a large number of states. In the second part of the thesis, we study the time-bounded reachability problem for CTMDPs, and propose (1) a conditional decidability result, and (2) a systematic method for improving scalability of numerical approximation methods.
Finally, we study the class of linear dynamical systems, which are fundamental models in many different domains of science and engineering. In the third part of this thesis proposal, we consider several reachability-related problems for linear dynamical systems, and propose (1) a hardness result for point-to-point reachability of linear dynamical systems with hyper-rectangular control sets, (2) decidability of pseudo-reachability for hyperplane target sets, and (3) decidability of pseudo-reachability for semi-algebraic target sets


--email hidden

Virtual Meeting Details

923 6785 8852
passcode not visible
logged in users only

Maria-Louise Albrecht, 01/26/2023 11:09
Maria-Louise Albrecht, 12/12/2022 16:09 -- Created document.