This project aims to develop design methodology for feedback control algorithms that satisfy complex safety and performance requirements. Rigorous design tools that meet such requirements are of utmost importance in manufacturing, autonomous vehicles, and infrastructure systems, such as smart cities, traffic networks, the power grid and water networks. The growing sophistication of these systems demand equally sophisticated control methods that are applicable to the complex requirements and large-scale models describing their operation. The project addresses this demand with a combination of tools from control theory, which traditionally deals with feedback regulation of dynamical systems around desired set points or trajectories, and formal methods used for verification of software and hardware systems. Merging tools from these areas is an exciting research opportunity but relies on a symbolic representation of continuous dynamical systems studied in control theory to be compatible with the models used in formal methods. Existing tools for obtaining symbolic representations require computations that do not scale well to large systems. To overcome this problem the project will exploit structural system properties inherent to classes of dynamical systems and eliminate key computational bottlenecks. The results will be demonstrated on autonomous docking of ships, a challenging maneuver that continues to be performed manually due to the high risk of collision combined with strict requirements for precision. This system is representative of a wide range of other applications and is an excellent test bed for control algorithms that meet complex requirements.
Symbolic control is an increasingly popular approach that translates the control synthesis problem from the continuous- to the discrete-state domain, allowing the designer to address complex control requirements expressed as automata or temporal logic formulas. Indeed, for finite discrete-state transition models, such as those that arise in software and hardware verification and synthesis, the formal methods community has developed number of efficient algorithmic tools to enforce such requirements. Bringing these tools to control theory is an exciting opportunity, but the computations involved in the design procedure do not scale well to systems with large state dimension and complex, nonlinear dynamics. This project aims to overcome key computational bottlenecks and achieve scalability by exploiting structural system properties. The research tasks include: 1) Developing scalable and broadly applicable reachability analysis methods, which are needed when obtaining a discrete-state representation of a continuous-state system; 2) Exploiting sparsity structures and symmetries intrinsic to the dynamical model to dramatically reduce the number of times that reachability computations are invoked, 3) Further improving scalability by first reducing the order and complexity of the dynamical model with a rigorous procedure offering guaranteed error bounds. Successful completion of these research tasks would elevate symbolic control to become a broadly applicable tool for safety-critical systems with complex, nonlinear dynamics. The results of the project will be demonstrated on autonomous docking of ships, a challenging maneuver that continues to be performed manually due to the high risk of collision combined with strict requirements for precision.
This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.
