这篇文档属于类型a，即报告了一项原创性研究。以下是对该研究的学术报告：

作者及研究机构

本研究的作者包括Huawei Xie（福建警察学院法医科学系及工程研究中心）、Jing Liu（西南交通大学消防工程系）和Na Li（福建警察学院公安系）。该研究于2024年发表在《The Computer Journal》上，DOI为10.1093/comjnl/bxae077。

学术背景

本研究的主要科学领域是离散事件系统（Discrete Event Systems, DES）中的不透明性（Opacity）问题。不透明性是系统安全与隐私中的一个重要属性，指的是系统的预设秘密行为不会被外部入侵者推断出来。在部分可观测的离散事件系统中，如何确保系统的不透明性是一个关键问题。本研究的目标是在标记Petri网（Labeled Petri Nets, LPNs）框架下，研究不透明性的验证与强制执行问题，并提出一种最大允许的监督器（Maximally Permissive Supervisor）来确保系统的不透明性。

研究流程

研究分为以下几个主要步骤：

1. 不透明性基础可达图（Opacity Basis Reachability Graph, OBRG）的构建
   首先，研究者开发了一种称为不透明性基础可达图（OBRG）的结构，用于表示系统的可达集，而不需要计算所有可达状态。OBRG包含了系统的不透明性信息，能够在不枚举所有标记的情况下，表示系统的行为。

2. 观察器（Observer）的计算
   基于OBRG，研究者计算了系统的观察器。观察器中的某些状态被定义为禁止状态（Forbidden States），并通过一个定理来验证系统的不透明性。该定理通过检查禁止状态来确定系统是否满足不透明性。

3. 不透明性监督器的设计
   对于不满足不透明性的LPN系统，研究者提出了一种最大允许的监督器，通过限制系统的行为来确保受控系统的不透明性。该监督器能够在不过度限制系统行为的情况下，强制执行不透明性。

研究结果

1. OBRG的有效性
   通过构建OBRG，研究者成功避免了计算所有可达标记的问题，显著减少了计算复杂度。实验结果表明，OBRG能够有效表示系统的不透明性信息。

2. 不透明性验证
   基于OBRG和观察器，研究者提出了一个必要且充分的条件来验证LPN系统的不透明性。通过检查观察器中的禁止状态，研究者能够确定系统是否满足不透明性。

3. 监督器的性能
   对于不透明的系统，研究者设计的最大允许监督器能够有效限制系统的行为，确保受控系统的不透明性。实验表明，该监督器在不透明性强制执行方面表现出色，且不会过度限制系统的行为。

结论

本研究在LPN框架下，提出了一种新的方法来验证和强制执行系统的不透明性。通过构建OBRG和观察器，研究者能够在不枚举所有可达状态的情况下，验证系统的不透明性。此外，提出的最大允许监督器能够有效限制系统的行为，确保受控系统的不透明性。该研究在系统安全与隐私领域具有重要的理论和应用价值。

研究亮点

1. 新颖的OBRG结构
   OBRG的提出避免了计算所有可达标记的问题，显著降低了计算复杂度。

2. 最大允许监督器
   研究者提出的监督器能够在确保不透明性的同时，最大程度地保留系统的行为，具有较高的应用价值。

3. 理论验证
   通过定理和算法，研究者提供了不透明性验证的严格理论支持，确保了方法的正确性和有效性。

其他有价值的内容

研究者在案例研究中，通过一个制造系统的例子展示了所提出方法的有效性。实验结果表明，该方法在处理大规模系统时，能够显著减少计算复杂度，且在实际应用中具有较高的可行性。

本研究在离散事件系统的不透明性验证与强制执行方面取得了重要进展，为系统安全与隐私领域提供了新的理论工具和实际应用方法。