Combining Optimality and Correctness in Control Systems

最优控制是一个工程领域，专注于保持系统接近预期行为，同时以相同的优化成本。例如，在最小化燃料消耗的同时沿着轨迹驾驶车辆，控制建筑物中的一组恒温器，使其遵循所需的温度曲线，同时将电力消耗保持在最低限度，等等。形式验证是计算机科学的一个领域，专注于证明系统设计的正确性。系统是计算机程序和数字电路，而正确性规范包括安全性（确保没有坏事发生）和活跃性（确保好事最终会发生）。随着物理和数字系统越来越多地集成到安全关键的网络物理系统中，需要结合最优控制和正确性要求的计算工具。该项目建立了最优控制和正式验证之间的联系，并影响了正确性和最优性至关重要的大量领域，例如空中交通管制（为飞机在拥挤的机场起飞和降落设计安全的最小能量路径），车辆自主（例如，持续监视救灾），医疗机器人（最优性和安全性是机器人针转向问题的基础）等。教育和推广计划包括本科和研究生阶段的相关课程，本科生和高中生参与研究，与小学机器人团队合作，以及首席研究员参与高中暑期实习项目。该项目的结果将包括最优控制问题的公式和解决方案，其正确性要求表示为有限和无限系统的时间逻辑公式，在概率和非概率设置中。所考虑的系统是有限状态转移系统和马尔可夫决策过程，以及无限状态离散时间（随机）线性系统和分段仿射系统。正确性被指定为线性时间逻辑的公式。优化目标包括经典的每阶段平均成本、状态变量和控制变量的二次方程，以及由特定规格引起的一些特殊成本。该方法的核心是最优控制策略的后退视界实现。主要应用领域是灾害救援场景中自动驾驶车辆的搜索和救援控制。

Optimal control is an area of engineering focused at maintaining systems close to desired behaviors, while at the same optimizing certain costs. Examples include driving a vehicle along a trajectory while minimizing fuel consumption, controlling a set of thermostats in a building to follow a desired temperature profile while maintaining electricity consumption to a minimum, etc. Formal verification is an area of computer science focused at proving the correctness of system designs. The systems are computer programs and digital circuits, while correctness specifications include safety (making sure nothing bad happens) and liveness (making sure something good eventually happens). With the increasing integration of physical and digital systems into safety critical cyber physical systems, there is a need for computational tools that combine optimal control and correctness requirements. This project establishes a connection between optimal control and formal verification and impacts a large number of areas where correctness and optimality are crucial, such as air traffic control (design safe minimum-energy paths for airplanes taking off and landing in a crowded airport), vehicle autonomy (e.g., persistent surveillance for disaster relief), medical robotics (optimality and safety are fundamental in the robotic needle steering problem), etc. The education and outreach plan includes related courses at the undergraduate and graduate level, the involvement of undergraduate and high school students in research, collaborations with elementary school robotics teams, and the involvement of the Principal Investigator in high school summer internship programs.The results of this project will include formulations and solutions to optimal control problems with correctness requirements expressed as temporal logic formulas for both finite and infinite systems, in both probabilistic and non-probabilistic setups. The systems under consideration are finite-state transition systems and Markov decisions processes, and infinite-state discrete-time (stochastic) linear systems and piecewise affine systems. Correctness is specified as formulas of Linear Temporal Logic. The optimization objectives include classical average costs per stage and quadratics over state and control variables, as well as some special costs induced by particular specifications. Central to the approach are receding-horizon implementations of the optimal control strategies. The main application area is autonomous vehicle control for search and rescue in disaster relief scenarios.