用于信息物理系统形式化建模与验证的混合自动机

离散控制（“赛博”）与模拟环境（“物理”）之间通过有线或无线通信网络上的传感器与执行器紧密集成，是信息物理系统的决定性特征。因此，信息物理系统的功能正确性不仅关键依赖于模拟物理环境的动力学，也依赖于改变环境动力学的离散控制所作出的决策。混合自动机框架——由 Alur、Courcoubetis、Henzinger 与 Ho 提出——提供了一种形式化建模与规约环境，用以分析信息物理系统离散与连续部分间的交互。混合自动机可视为有限状态自动机的推广，其增强了有限组实值变量，这些变量在每一状态下的动力学由常微分方程组支配。此外，混合自动机的离散转移由这些实值变量取值上的约束守卫，并允许这些变量演化中的不连续跳跃。考虑到混合自动机中动力学的丰富性，通用模型的基本验证问题（如可达性与可调度性）不可判定或许并不令人意外。本文中我们综述混合自动机作为信息物理系统建模与验证框架的应用，并调研与混合自动机实际验证问题相关的若干关键结果。