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.