Mahmoud Salamati

• 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 disturbance, such as measurement noise and mismatch between the dynamics of the physical system and its model. 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. For some specific classes of systems, we provide sound and complete decision procedures. For general nonlinear dynamical systems for which undecidability of basic synthesis problems is proven, we propose sound but scalable technique that can be applied to the real-world dynamical systems. First, we consider continuous dynamical systems with bounded disturbances. 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 disturbances is known. A promising 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 reduce 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 set of states 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 for scaling up 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, 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, and (2) decidability of pseudo-reachability for hyperplane target sets.