将模块系统中的不透明性验证转化为非阻塞验证
计算机科学中的逻辑
2019-05-14 v2 形式语言与自动机理论
摘要
我们考虑以交互式非确定性有限状态自动机建模的系统的当前状态与 K 步不透明性的验证。我们描述了一种用于组合式不透明性验证的新方法，其采用一种称为不透明观测等价性的抽象概念，并利用已有的组合式非阻塞验证算法。该组合式方法基于系统的一种变换，其中变换后的系统是非阻塞的当且仅当原系统是当前状态不透明的。此外，我们证明若变换后的系统是非阻塞的，则也可推断 K 步不透明性。我们给出了实验结果为大规模扩展系统的当前状态不透明性提供了高效验证。
引用
@article{arxiv.1904.06242,
title = {Transforming opacity verification to nonblocking verification in modular systems},
author = {Sahar Mohajerani and Stephane Lafortune},
journal= {arXiv preprint arXiv:1904.06242},
year = {2019}
}