Pushing the Barriers in Controller Synthesis for Cyber-Physical Systems

The thesis has three main parts: In the first part, we address the scalability bottleneck of the existing ABCD procedures by using a multi-layered abstraction of varying granularities. We implemented this multi-layered ABCD algorithm in the tool called Mascot, using which we empirically demonstrate the significant saving in computation time achieved through our approach. In the second part of the thesis, we propose a modular design procedure of sound local controllers for a network of discrete abstract systems communicating via discrete/boolean variables and having local specifications. We propose a sound algorithm, where the abstractions negotiate a pair of local assume-guarantee contracts (and controllers as a by-product), in order to synchronize on a set of non-conflicting and correct behaviors. We show the effectiveness of our algorithm using a prototype tool, called Agnes, on a set of discrete benchmark examples. In the third part, we present a novel ABCD procedure for discrete-time nonlinear stochastic control systems and omega-regular control specifications. We first present a novel 2.5-player game abstraction for the control problem at hand. Alongside our abstraction, we present a direct and efficient symbolic algorithm for solving 2.5-player games for omega-regular specifications. We implemented our algorithms in a prototype tool called Mascot-SDS, using which we empirically show that our approach is both faster and more memory-efficient than an alternate approach that was independently developed around the same time.