Scalable Symbolic Control: Computationally Efficient Design of Feedback Control Algorithms to Satisfy Complex Requirements

可扩展符号控制：满足复杂要求的反馈控制算法的计算效率设计本项目旨在开发满足复杂安全和性能要求的反馈控制算法的设计方法。满足这些要求的严谨设计工具在制造业、自动驾驶汽车和智能城市、交通网络、电网和供水网络等基础设施系统中至关重要。这些系统的日益复杂需要同样复杂的控制方法，这些方法适用于复杂的要求和描述其操作的大规模模型。该项目结合了控制论的工具和用于验证软件和硬件系统的形式化方法，满足了这一需求。控制论传统上处理动态系统围绕所需设置点或轨迹的反馈调节。合并这些领域的工具是一个令人兴奋的研究机会，但依赖于控制理论中研究的连续动力系统的符号表示法，以与形式方法中使用的模型兼容。现有的用于获得符号表示的工具需要的计算不能很好地扩展到大型系统。为了克服这个问题，该项目将利用动力系统类固有的结构系统属性，并消除关键的计算瓶颈。结果将在船舶自动对接上得到展示，这是一种具有挑战性的操作，由于高碰撞风险和对精度的严格要求，这种操作仍需手动执行。该系统代表了广泛的其他应用，是满足复杂要求的控制算法的极好试验台。符号控制是一种日益流行的方法，它将控制综合问题从连续域转换到离散状态域，允许设计者解决以自动机或时序逻辑公式表示的复杂控制要求。事实上，对于有限的离散状态转换模型，例如在软件和硬件验证和综合中出现的模型，形式方法社区已经开发了许多有效的算法工具来执行这些要求。将这些工具引入控制理论是一个令人兴奋的机会，但设计过程中涉及的计算不能很好地扩展到具有大状态维和复杂的非线性动力学的系统。该项目旨在克服关键的计算瓶颈，并通过利用结构系统属性实现可伸缩性。研究任务包括：1)开发可伸缩的和广泛适用的可达性分析方法，这是获得连续状态系统的离散状态表示时所需要的；2)利用动力学模型固有的稀疏性结构和对称性来显著减少调用可达性计算的次数；3)通过首先降低动力学模型的阶数和复杂性来进一步提高可伸缩性，并通过严格的过程提供保证的误差界。成功完成这些研究任务将提升符号控制，使其成为具有复杂、非线性动态的安全关键系统的广泛应用工具。该项目的结果将在船舶自动对接上得到展示，这是一种具有挑战性的操作，由于高碰撞风险和对精度的严格要求，这种操作仍然需要手动执行。这一奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Scalable Symbolic Control: Computationally Efficient Design of Feedback Control Algorithms to Satisfy Complex RequirementsThis 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.