Modern autonomous systems such as autonomous vehicles and robotic manipulators rely on machine learning to handle complex dynamics and adapt to uncertain environments. However, learning-based components are typically “black boxes,” making it challenging to provide the formal guarantees required in safety-critical applications. Our research develops verified learning-based control methods that integrate machine learning, control theory and formal methods. Read more
Over the past decade, numerous controller synthesis approaches have emerged by combining tools from control theory and formal methods. Formal methods originated in computer science, where system models are typically simple but specifications are complex, often expressed using temporal logic. In contrast, control theory deals with complex continuous-time models with relatively simple specifications. The standard bridge between the two fields, known as symbolic control, consists in abstracting continuous-state dynamical systems into discrete-state transition models, enabling controller synthesis in the discrete domain. Read more
Machine learning models are now used in many important areas, from healthcare and finance to autonomous systems and natural language processing. However, the robustness of these models remains a critical concern: how will they behave when confronted with adversarial examples, distribution shifts, corrupted or missing data, or subtle implementation errors? Without strong robustness guarantees, ML systems risk failure, liability, and lack of trust. Read more
Modern cyber–physical systems, such as autonomous multi-agent teams, networked infrastructures, and hybrid dynamical systems are increasingly large, interconnected, and heterogeneous. Ensuring correct and safe behavior in such systems is challenging because global verification and centralized controller synthesis often scale poorly with dimension, communication constraints, and subsystem coupling. Our work leverages assume–guarantee contracts as a principled framework to decompose complex control and verification tasks into manageable components. Read more
Safety-critical systems, such as autonomous vehicles, robots and power systems must stay within safe limits despite uncertainties and disturbances, which makes ensuring reliable operation challenging. Robust controlled invariant sets are used to formalize this notion of safety by identifying all states from which the system can be kept safe indefinitely through admissible control actions, regardless of disturbances. Read more
In safety-critical applications, disturbances and unexpected events are unavoidable, making the ability of control systems to remain operational a fundamental requirement. In our work, we define resilience as the largest set of admissible disturbances under which a system can still satisfy complex specifications. Our work focuses on the resilience analysis and synthesis of control systems, developing methods to quantify, guarantee, and maximize the performance of controlled dynamical systems under real-world perturbations. Read more
Modern power systems are undergoing a paradigm shift with the integration of distributed renewable energy sources, electrification across diverse infrastructures (such as buildings and transportation hubs), and the deployment of intelligent grid-edge technologies. In this context, cyber-physical energy systems like multi-zone buildings and microgrids are evolving from passive consumers into active agents that participate in demand-side flexibility, grid stabilization, energy arbitrage, and market optimization. Read more
Large-scale dynamical systems arise naturally in many modern infrastructures, with power and social networks among the most prominent examples. These systems consist of thousands or even millions of interconnected components whose collective behavior evolves. Their scale, complexity, and heterogeneity create fundamental challenges for analysis, control, and real-time decision-making. Our work focuses on those large-scale systems, where high dimensionality often creates severe bottlenecks in sensing, actuation, computation, and communication. We investigate how to introduce randomized compression and sparsity into the structure of large-scale systems, such as through reduced sensing, selective actuation, or compressed updates, while still guaranteeing key control objectives, including stability, convergence, and robustness. Read more