Compositional and Abstraction-Based Approach for Synthesis of Edit Functions for Opacity Enforcement
Compositional and Abstraction-Based Approach for Synthesis of Edit Functions for Opacity Enforcement
复制标题
DOI：
10.1109/tac.2019.2946165
复制
发表时间：
2019-10
影响因子：
6.8
通讯作者：
Sahar Mohajerani;Yiding Ji;S. Lafortune
中科院分区：
文献类型：
--
作者：
Sahar Mohajerani;Yiding Ji;S. Lafortune
本文开发了一种新颖的基于组合和抽象的方法来综合编辑功能，以在模块化离散事件系统中执行不透明度。编辑功能通过删除或插入事件来改变系统的输出，以迷惑外部入侵者，其目标是从观察中推断出系统的秘密。我们综合编辑功能来解决模块化设置中的不透明度强制问题，与整体方法相比，这显着降低了计算复杂性。首先采用两种称为不透明观察等价和不透明互模拟的抽象方法来抽象模块化系统的各个组件及其观察者。随后，我们提出了一种将编辑函数的综合转化为模块化至上非阻塞管理器的计算的方法。我们证明以这种方式合成的编辑函数正确地解决了不透明度强制问题。
This article develops a novel compositional and abstraction-based approach to synthesize edit functions for opacity enforcement in modular discrete event systems. Edit functions alter the output of the system by erasing or inserting events in order to obfuscate the outside intruder, whose goal is to infer the secrets of the system from its observation. We synthesize edit functions to solve the opacity enforcement problem in a modular setting, which significantly reduces the computational complexity compared with the monolithic approach. Two abstraction methods called opaque observation equivalence and opaque bisimulation are first employed to abstract the individual components of the modular system and their observers. Subsequently, we propose a method to transform the synthesis of edit functions to the calculation of modular supremal nonblocking supervisors. We show that the edit functions synthesized in this manner correctly solve the opacity enforcement problem.