通过近似双相似有限抽象对随机系统进行符号控制

针对复杂系统的控制设计的符号方法采用构建与原始控制系统相关的有限状态模型，然后利用有限状态综合技术计算满足时态逻辑给定规范的控制器，最后将综合出的方案转换回具体复杂系统的控制器。此类方法已成功开发并应用于非概率控制系统的控制器综合。在本文中，我们将该技术扩展到由受控随机微分方程建模的概率控制系统。我们表明，对于每一个满足增量输入到状态稳定性的概率变体的随机控制系统，以及对于每一个给定的精度 $\varepsilon>0$，都可以构建一个有限状态转移系统，该系统在矩的意义下与原始随机控制系统是 $\varepsilon$-近似双相似的。此外，我们提供了关于随机控制系统与其相应有限状态转移系统之间关系的结论，这些关系基于文献中已知的概率双模拟关系。我们通过为用线性时态逻辑表达的丰富规范综合随机控制系统的控制器，展示了该构建方法的有效性。所讨论的技术为随机控制系统启用了一种新的、自动化的、构造即正确的控制器综合方法，这类系统是许多受结构化不确定性影响的安全关键系统中常用的数学模型，因此与控制物理应用密切相关。