连续状态动力学系统的多分辨率近似双仿射构成的存在性与综合

我们提出了一个完全自动的框架，用于合成在给定局部分辨率要求下的确定性连续状态自治系统的紧凑、有限状态确定性抽象。我们的做法建立在多分辨率近似双仿射（multi-resolution approximate bisimulations）之上，这是经典 $\epsilon$ -近似双仿射的泛化，支持状态依赖的误差界并涵盖了可变分辨率关系和均匀分辨率关系。我们指出，某些系统可接受多分辨率双仿射，但不存在 $\epsilon$ -近似双仿射。我们证明了所有递增均匀有界 ($\delta$ -UB) 系统都存在多分辨率近似双仿射等价抽象，从而扩大了符号验证的适用范围以覆盖更广泛的动力学系统；作为一个平凡的特例，这一结果也涵盖了递增全局渐近稳定 ($\delta$ -GAS) 系统。通过可扩展的仪表驱动的归纳综合 (CEGIS) 循环求解多分辨率抽象综合问题 (MRASP)，结合网格细化与反例驱动的细化，确保所有 $\delta$ -UB 系统的正确性，并在某些特殊情况下确保终止。在线性和非线性基准（包括非 $\delta$ -GAS 和不可导的情况）上的实验表明，我们的算法在实施更紧密、位置依赖的误差保证的同时，生成的抽象可比基于李雅普诺夫的网格小幅度（最高可达 50%）更紧凑。