切换系统初始状态不透明性的组合验证
系统与控制
2021-09-27 v1 系统与控制
摘要
在这项工作中,我们提出了一种用于验证离散时间切换系统网络的近似初始状态不透明性的组合框架。所提方法基于近似初始状态不透明性保持仿真函数(InitSOPSF)的概念,其刻画了具体网络与其有限抽象在满足近似初始状态不透明性方面的接近程度。我们证明了通过假设某些小增益型条件并组合为每个子系统分别构建的所谓局部 InitSOPSF,可以组合地获得此类 InitSOPSF。此外,对于满足某些稳定性性质的切换系统,我们提供了一种构建其有限抽象及相应局部 InitSOPSF 的方法。最后,通过一个例子说明了我们结果的有效性。
引用
@article{arxiv.2109.12024,
title = {Compositional Verification of Initial-State Opacity for Switched Systems},
author = {Siyuan Liu and Abdalla Swikir and Majid Zamani},
journal= {arXiv preprint arXiv:2109.12024},
year = {2021}
}
备注
This paper has been accepted and published in CDC 2020. arXiv admin note: substantial text overlap with arXiv:2006.16661