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

主要作者及研究机构

本研究的主要作者包括Yin Tong（西安电子科技大学）、Zhiwu Li（澳门科技大学和西安电子科技大学）、Carla Seatzu（卡利亚里大学）和Alessandro Giua（艾克斯-马赛大学和卡利亚里大学）。该研究发表于IEEE Transactions on Automatic Control期刊，2021年6月第62卷第6期。

学术背景

本研究的主要科学领域是离散事件系统（Discrete Event Systems, DES），特别是基于Petri网（Petri Nets）的状态不透明性（State-based Opacity）验证。不透明性（Opacity）是信息安全领域的一个重要概念，指系统在部分可观测的情况下，外部入侵者无法确定系统的秘密行为。Petri网作为一种强大的建模工具，能够有效描述离散事件系统的动态行为。然而，尽管Petri网在建模方面具有优势，但关于其在状态不透明性验证中的应用研究仍然较少。本研究旨在提出一种基于基础可达图（Basis Reachability Graph, BRG）的高效方法，用于验证Petri网中的当前状态不透明性（Current-State Opacity）和初始状态不透明性（Initial-State Opacity），从而避免传统方法中因状态空间爆炸（State Explosion）带来的计算复杂性。

研究流程

本研究的主要流程包括以下几个步骤：

1. 问题定义与背景知识
   研究首先定义了状态不透明性的两种形式：当前状态不透明性和初始状态不透明性。当前状态不透明性指入侵者无法确定系统的当前状态是否属于秘密状态，而初始状态不透明性指入侵者无法确定系统的初始状态是否属于秘密状态。研究假设入侵者已知系统的结构和初始标记，但只能部分观测系统的事件发生。

2. Petri网建模与基础可达图构建
   研究采用标记Petri网（Labeled Petri Net, LPN）作为系统模型，其中观测函数是静态的，且状态不可观测。为了高效验证不透明性，研究引入了基础可达图（BRG）的概念。BRG是Petri网可达图的一种紧凑表示，仅枚举基础标记（Basis Markings），而非所有可达标记。BRG的构建通过算法1实现，该算法递归地计算基础标记及其之间的转移关系。

3. 当前状态不透明性验证
   研究提出了基于BRG的当前状态不透明性验证方法。首先，定义了暴露标记（Exposable Markings）和弱暴露标记（Weakly Exposable Markings）的概念，并证明了当前状态不透明性的充要条件。接着，研究开发了当前状态基础观测器（Current-State Basis Observer），通过将BRG转换为确定性有限自动机（DFA）来验证不透明性。此外，研究还讨论了当秘密由广义互斥约束（Generalized Mutual Exclusion Constraints, GMECs）描述时，如何通过整数线性规划（ILP）问题简化验证过程。

4. 初始状态不透明性验证
   研究将初始状态不透明性验证问题扩展到Petri网中，提出了基于BRG的验证方法。研究定义了初始状态估计器（Initial-State Estimator），并通过构建BRG的初始状态观测器来验证不透明性。此外，研究还提出了修改基础可达图（Modified Basis Reachability Graph, MBRG）的概念，用于处理不满足假设A3（即秘密标记的不可观测到达集也属于秘密）的情况。

5. 数值实验与工具开发
   研究通过一系列数值实验验证了所提方法的有效性，并开发了基于MATLAB的工具来支持BRG的构建、不透明性验证及相关分析。

主要结果

1. BRG的构建与验证
   研究成功构建了BRG，并通过数值实验证明了其在高维Petri网中的高效性。例如，当初始标记的参数k从8增加到100时，BRG的规模（基础标记数量）从19增加到203，而传统可达图的规模从220增加到13244，且当k=60时，传统方法因状态爆炸无法完成计算。

2. 当前状态不透明性验证
   研究提出的基于BRG的验证方法显著降低了计算复杂性。例如，当秘密由GMECs描述时，验证过程可通过求解ILP问题实现，进一步提高了效率。

3. 初始状态不透明性验证
   研究提出的MBRG方法成功解决了不满足假设A3的情况，并通过实验验证了其有效性。例如，当秘密包含弱暴露标记时，MBRG能够准确验证初始状态不透明性。

结论

本研究提出了一种基于BRG的高效方法，用于验证Petri网中的状态不透明性。该方法通过避免状态空间的穷举枚举，显著降低了计算复杂性，并能够处理更复杂的系统模型。研究还开发了MATLAB工具，为相关领域的研究者提供了实用的分析工具。

研究亮点

1. 高效性：通过引入BRG，研究成功避免了传统方法中的状态爆炸问题，显著提高了验证效率。
2. 通用性：研究提出的方法不仅适用于当前状态不透明性验证，还可扩展到初始状态不透明性验证。
3. 实用性：研究开发的MATLAB工具为Petri网的不透明性验证提供了实用的技术支持。

其他有价值的内容

研究还讨论了入侵者对初始标记的不确定性情况，并提出了扩展观测器（Extended Observer）的概念，用于处理此类复杂场景。此外，研究还提供了详细的数值实验结果，验证了所提方法在不同参数下的有效性。