从小增益理论到大规模随机系统障碍证书的组合式构造

本文关注一种组合式方法，用于为大规模互联随机系统构造控制障碍证书，同时针对高层逻辑性质合成混合控制器。我们提出的方法将互联系统分解为较小的子系统，并利用子系统的控制子障碍证书概念，通过采用某些极大型小增益条件来构造互联系统的控制障碍证书。主要目标是在有界时间范围内给定规范满足的概率保证下，合成强制复杂逻辑性质（包括由确定性有限自动机接受语言表示的性质）的混合控制器。为此，我们提出一种系统方法，首先利用对应于规范补的自动机将高层规范分解为简单可达性任务。然后我们构造控制子障碍证书并为这些更简单的任务合成局部控制器，将其组合以获得确保以某概率下界满足复杂规范的混合控制器。为计算控制子障碍证书及相应局部控制器，我们提供基于平方和（SOS）优化程序和反例引导归纳合成（CEGIS）框架的两种系统方法。最后我们将所提技术应用于两个物理案例研究。