拉格朗日动力学形式化及其在机器人验证中的应用

拉格朗日动力学是很多学科和工程的基础理论，应用非常广泛。包括机器人系统等很多动力学系统是安全攸关系统，需要进行严格的正确性和可靠性验证。形式化拉格朗日动力学是进行动力学理论推导和动力学系统形式化验证的基础。目前国际上对形式化数学的研究关注度很高，但是动力学理论的形式化尚属空白。本项目研究拉格朗日动力学的高阶逻辑形式化理论，并以机器人为例研究动力学系统的形式化分析与验证的方法，具体包括：连续可微函数空间、泛函与变分、最小作用原理的形式化表达和证明；虚功原理、达朗贝尔原理、动力学普遍方程和哈密顿原理的形式化表达和证明；拉格朗日量、两类拉格朗日方程的形式化表达和证明；基于拉格朗日动力学理论的机器人机构动力学形式化分析与验证方法。本项目将实现国际上第一个拉格朗日动力学高阶逻辑程序库，实现基于拉格朗日动力学的机器人动力学形式化分析与验证的工具包。

As the theoretical foundation for a great number of sub-disciplines of science and engineering, Lagrangian dynamics has extensive applications in science and engineering. Many dynamic systems (e.g., robotic systems) are safety-critical; hence, it is highly beneficial to conduct rigorous verification of these systems, thereby ensuring their correctness and reliability. To enable computerized derivation of theoretical results on Lagrangian dynamics and to conduct formal verification of dynamic systems, the formalization of Lagrangian dynamics is a pre-requisite. Currently, the formalization of mathematics is drawing a high amount of attention on an international scale. However, the formalization of dynamic theory in particular, remains a hitherto unexplored area. In this project, we will investigate the formalization of Lagrangian dynamics using higher-order logics (HOL). Furthermore, we will develop methodologies for the formal analysis and verification of dynamic systems with robotic systems as a specific application domain. The concrete problems we will address include: the formalization of continuous differentiable function spaces, functional analysis and variational methods, and the least action principle; the formalization of the principle of virtual work, D'Alembert's principle, the general equation of dynamics, and Hamilton principle; the formalization of the Lagrangian function and the two types of Lagrangian equations; and the formal analysis and verification of the dynamic design of robotic mechanisms based on Lagrangian dynamics. In this project, we will fill a gap in the formal verification of Lagrangian dynamic systems by developing the first (HOL-based) library of formal definitions and proofs for Lagrangian dynamics, and by implementing a tool kit for the formal analysis and verification of robot dynamics.