本文研究部分可观测离散事件系统中的匿名性验证问题。匿名性是一种信息流安全属性，其核心思想是：在外部观察者通过系统输出（观测）推断系统内部状态时，系统不应让某一时刻的状态被唯一确定，从而保护用户隐私。在离散事件系统框架下，已有 K-步匿名性和无限步匿名性的定义：K-步匿名性要求当前时刻之前至多 K 个观测步内，状态估计不能是单例；无限步匿名性则不对 K 设限。作者针对由非确定有限状态自动机建模的部分可观测系统，提出了四种新的匿名性概念——两种强匿名性和两种弱匿名性，分别称为 K-步强/弱匿名性和无限步强/弱匿名性。这些概念与已有定义的本质区别在于引入了强匿名投影与弱匿名投影的考量，使匿名性刻画更加精细，能够适应不同的隐私需求。为了验证这四种性质，作者发展了一套基于并发组合（concurrent composition）的新方法：通过构造系统的并发组合结构，系统性地追踪观测一致的状态对/状态集，从而将匿名性验证转化为对组合图的结构性质检查。基于该结构，论文给出了四种匿名性可验证的充要条件，并分析了相应算法的时间复杂度。此外，还计算了 K-步强匿名性和弱匿名性中 K 的上界，为实际应用中选择合适的匿名窗口提供了理论依据。本文属于形式化方法与信息流安全的交叉方向，适合从事隐私验证、自动机理论、安全协议分析的研究人员阅读。由于仅有摘要，具体定理证明与实验评估细节需参见全文。