论文标题
线性随机系统的相似性定量：耦合补偿器方法
Similarity quantification for linear stochastic systems: A coupling compensator approach
论文作者
论文摘要
对于控制系统的正式验证和设计，具有量化精度的抽象至关重要。当考虑随机连续状态模型与其有限（减少阶）抽象之间的准确偏差界限时，尤其如此。在这项工作中，我们引入了一个耦合补偿器来参数化相关耦合集，并为线性随机系统提供了全面的计算方法和分析。更确切地说，我们开发了一种计算方法，该方法表征了可能的模拟关系集，并在系统输出和过渡概率中的偏差方面的误差贡献之间进行了权衡。我们展示了此错误权衡对案例研究的保证满意度概率的影响，在该案例研究中，将正式规范作为时间逻辑公式提供。
For the formal verification and design of control systems, abstractions with quantified accuracy are crucial. This is especially the case when considering accurate deviation bounds between a stochastic continuous-state model and its finite (reduced-order) abstraction. In this work, we introduce a coupling compensator to parameterize the set of relevant couplings and we give a comprehensive computational approach and analysis for linear stochastic systems. More precisely, we develop a computational method that characterizes the set of possible simulation relations and gives a trade-off between the error contributions on the systems output and deviations in the transition probability. We show the effect of this error trade-off on the guaranteed satisfaction probability for case studies where a formal specification is given as a temporal logic formula.
