Comparing the Notions of Opacity for Discrete-Event Systems
不透明度是一种信息流特性，它表征了一个系统是否会向被动的观察者揭示它的秘密。在文献中已经引入了几个不透明度的概念。我们研究了基于语言的不透明度，当前状态不透明度，初始状态不透明度，初始和最终状态不透明度，K步不透明度和无限步不透明度的概念。比较这些概念是一个自然的问题，Wu和Lafortune对此进行了研究和总结，他们提供了当前状态不透明性、初始和最终状态不透明性和基于语言的不透明性之间的转换，对于前缀封闭的语言，还提供了基于语言的不透明性和初始状态不透明性之间的转换。我们扩展这些结果表明，所有讨论的概念的不透明度是相互转化。除了更深入地了解概念之间的差异外，变换还可以应用于复杂性结果。特别是，变换是可计算的多项式时间，并保持可观察的事件和确定性的数量，因此计算复杂性的验证的概念相吻合。我们提供了一个完整的和改进的复杂性图片所讨论的概念的不透明度的验证，并提高算法的复杂性，决定基于语言的不透明度，无限步不透明度，和K步不透明度。
2021-06-26 cs.FL cs.SY eess.SY
Complexity of Detectability, Opacity and A-Diagnosability for Modular Discrete Event Systems
Czech Academy of Sciences（捷克科学院）；Shanghai Jiao Tong University（上海交通大学）
本文研究模块化离散事件系统中检测性、保密性和A诊断性的复杂性，证明其比单体系统更复杂，为EXPSPACE完全问题，特殊情况下为PSPACE完全。
2017-10-08 cs.FL cs.SY eess.SY
Opacity in Discrete Event Systems: A Perspective and Overview
School of Automation and Intelligent Sensing, Shanghai Jiao Tong University（上海交通大学生物医学工程学院）
本文综述了离散事件系统中不透明性的定义、核心概念、验证技术及应用，探讨了不同观察模型对问题解决的影响及未来挑战。
2026-02-26 cs.FL cs.SY eess.SY
Opacity of Parametric Discrete Event Systems: Models, Decidability, and Algorithms
Guangdong University of Finance（广东金融学院）
本文针对参数化离散事件系统，提出扩展有限自动机（EFAs）和事件参数EFAs（EP-EFAs）两种模型，证明前者表达能力更强且不透明性一般不可判定，并为后者给出当前状态、初始状态和无限步不透明性的验证算法与复杂度分析。
2023-07-08 cs.FL cs.SY eess.SY
K-Step Opacity in Discrete Event Systems: Verification, Complexity, and Relations
不透明度是一种属性，表示系统是否可以向知道系统结构但对其行为观察有限的被动观察者（入侵者）透露其秘密。不透明度的几个概念已经被研究，包括当前状态不透明度，K步不透明度和无限步不透明度。我们研究了K步不透明性，概括了当前状态的不透明性和无限步不透明性，并询问入侵者是否不能决定，在任何时候，是否或当系统处于秘密状态在最后K个可观察的步骤。设计了一种新的K步不透明度判定算法，该算法的复杂度低于现有算法，且不依赖于K。然后，我们比较K步不透明度与其他不透明度的概念，并提供新的概念之间的转换，不使用状态，既不是秘密也不是非秘密（中性状态），这是多项式的系统的大小和二进制编码的K。
2021-09-05 cs.CR cs.FL cs.SY
Opacity of Discrete Event Systems with Active Intruder
不透明度是一种安全属性，它形式化地描述了系统对外部观察者（即入侵者）的信息泄漏。离散事件系统（DES）文献中研究的传统不透明性通常假设被动入侵者，他们只观察系统的行为。然而，在许多网络安全问题，如Web服务，主动入侵者，谁能够影响系统的行为超出被动的观察，需要考虑和防御。因此，我们有动机扩展不透明的概念来处理主动入侵者。为此，我们将系统建模为非确定性有限状态换能器。假设入侵者对系统结构有充分的了解，并且能够通过注入不同的输入并观察其响应来与系统进行交互。在这种设置中，我们首先引入反应性当前状态不透明度（RCSO）的概念，其特征在于系统不泄漏其秘密状态，无论入侵者如何操纵系统的行为。我们进一步扩展这个概念，以语言为基础的和初始状态的反应不透明的概念，并研究它们之间的关系。结果表明，所有提出的反应不透明度概念都等价于RCSO。因此，我们专注于RCSO和研究其验证问题。它表明，RCSO可以通过构造一个观察者自动机进行验证。
2020-07-24 cs.LO cs.SY eess.SY
Abstraction-Based Verification of Approximate Pre-Opacity for Control Systems
本文考虑离散时间控制系统的预不透明性的验证问题。预不透明性是一个重要的信息流安全属性，它保证了系统在未来执行某些秘密行为的意图。现有的预不透明性研究仅考虑非度量离散系统，假设入侵者能够精确区分不同的输出行为。然而，对于连续空间控制系统，其输出集配备有度量（这是大多数现实世界的应用程序的情况下），它是过于限制，以假设精确的测量从外部观察员。在本文中，我们首先引入了近似预不透明度的概念，通过捕获的安全水平的控制系统的测量精度的入侵者。基于这种新的概念的预不透明性，我们提出了一种验证方法，利用基于抽象的技术，连续空间控制系统。特别地，引入了近似预不透明度保持模拟关系的新概念，以保持预不透明度的方式来表征两个系统之间的距离。这种新的系统关系使我们能够验证复杂的连续空间控制系统使用其有限的抽象前不透明。在一定的稳定性假设下，我们还给出了一类离散时间控制系统的预不透明保持有限抽象的构造方法。
2022-11-08 cs.SC cs.SY eess.SY
Privacy-Preserving Supervisory Control of Discrete-Event Systems via Co-Synthesis of Edit Function and Supervisor for Opacity Enforcement and Requirement Satisfaction
本文研究了离散事件系统（DES）监督控制中编辑函数和监督器的协同综合问题，假设存在外部（被动）入侵者，其中需要达到以下目标：1）外部入侵者永远不应该推断系统秘密，即，系统是不透明的，并且永远不能确定编辑功能的存在，即，编辑功能保持隐蔽性; 2）在编辑功能存在的情况下，受控对象的行为应满足一定的安全性和非阻塞性要求。我们关注满足以下性质的编辑函数类：1）编辑函数的观察能力一般可以不同于监督者和入侵者的观察能力; 2）编辑函数可以实现插入、删除和替换操作; 3）编辑函数执行有界编辑操作，即，编辑函数的每个字符串输出的长度由给定常数限定上限。我们提出了一种方法来解决这个协同综合问题建模为一个分布式的监督合成问题的Ramadge-Wonham监督控制框架。考虑到这种分布式管理器合成问题的特殊结构，并提高找到非空分布式管理器的可能性，我们提出了两种新的合成算法，增量合成的管理器和编辑功能。我们的方法的有效性说明了一个例子中的位置隐私的执行。
2021-04-09 cs.SY eess.SY
Verification of infinite-step and K-step opacity Using Petri Nets
研究了离散事件系统的无限步不透明性和K步不透明性问题。一个Petri网系统被称为无限步/K步不透明的，如果它的所有秘密状态在无限步/K步内的任何时刻对入侵者都是不透明的。换句话说，入侵者永远无法确定，该系统曾经是在一个秘密的状态下，在无限/K步的基础上，它的观察系统的演变。基于基可达性和双向观测器的概念，提出了一种验证无限步不透明性和K步不透明性的有效方法。
2019-09-09 cs.SY eess.SY
Complexity of Verifying Nonblockingness in Modular Supervisory Control
TU Dresden（德累斯顿工业大学）；Institute of Theoretical Computer Science（理论计算机科学研究所）；cfaed（计算与工程数据科学中心）
本文研究模块化监督控制中非阻塞性验证的复杂度问题，结合复杂度理论结果，证明了非阻塞性相关的新结论。
2017-03-15 cs.FL cs.SY eess.SY
A Framework for Current-State Opacity under Dynamic Information Release Mechanism
不透明性是一个重要的信息流安全属性，它表征了动态系统对窃听攻击的“秘密”的合理可否认性。作为一种信息流属性，底层观测模型是不透明度建模和分析的关键。在本文中，我们研究了在Orwell型观测下离散事件系统的当前状态不透明性的验证，即，允许系统基于其未来后缀重新解释事件的观测。首先，我们提出了一个新的奥威尔式的观察模型称为动态信息发布机制（DIRM）。在DIRM中，何时释放先前的“保持”事件取决于状态。然后，我们提出了一个新的定义的不透明度的概念的基础上的历史等价，而不是标准的投影等价。此定义更适合于非前缀闭合的观测。最后，我们表明，通过构建一个新的结构称为DIRM观察者，当前状态的不透明性可以有效地验证下的DIRM。计算复杂性分析以及说明性的例子，所提出的方法也提供。与现有的Orwell型观测模型相比，该框架具有更一般的意义，即信息发布机制是状态依赖的，相应的不透明度定义更适合于非前缀闭观测。
2022-01-17 cs.FL cs.SY eess.SY
A Unified Framework for Verification of Observational Properties for Partially-Observed Discrete-Event Systems
本文研究部分可观测离散事件系统（DES）的性质验证问题。特别是，我们感兴趣的是验证与系统的信息流有关的观测性质。这里考虑的观测性质包括可诊断性，可预测性，可检测性和不透明性，这在文献中引起了相当大的关注。然而，在现有的结果，不同的验证程序开发不同的属性的情况下，在这项工作中，我们提供了一个统一的框架，验证所有这些属性，减少他们作为一个实例的HyperLTL模型检查。我们的方法是基于一个Kripke结构的建设，有效地捕捉问题的不可观测性，以及在部分观察DES的有限字符串语义，使HyperLTL模型检测技术可以适当地应用。然后，对于考虑的每个观测性质，我们明确提供了HyperLTL公式，以在Kripke结构上进行检查，以进行验证。我们的方法是统一的，在这个意义上，所有不同的属性可以验证相同的模型检查引擎。此外，我们的统一框架还带来了新的见解，部分观测DES的验证复杂性方面的观测属性进行分类。
2022-12-17 cs.SY eess.SY
A unified method to decentralized state inference and fault diagnosis/prediction of discrete-event systems
状态推断问题和故障诊断/预测问题是许多领域的基本课题。在本文中，我们考虑离散事件系统（DES）建模的有限状态自动机（FSA）。后一个问题的分散版本存在结果，但前一个问题的分散版本几乎没有结果。我们提出了一个分散版本的强可检测性称为co-detectability，这意味着一旦一个系统满足这一属性，对于每个生成的无限长的事件序列，至少有一个本地观察员可以确定当前和后续状态后，一个共同的观察时间延迟。我们证明了验证FSA的可检测性的问题是CONP困难的。此外，我们使用一个统一的并发合成方法，给出了PSPACE验证算法的可检测性，可诊断性，和可预测性的FSA，没有任何假设或修改的FSA正在考虑，其中可诊断性首先研究的[Debouk & Lafortune & Teneketzis 2000]，而可预测性首先研究的[Kumar \& Takai 2010]。通过我们提出的统一方法，可以看出，为了验证共同可检测性，与验证其他两个属性相比，将遇到更多的技术困难，因为在共同可检测性中，生成的输出被计数，但在后两个属性中，仅计数事件的发生。例如，当生成一个输出时，可能发生任何数量的不可观察事件。PSPACE-硬度验证共同诊断性是已知的文献。在本文中，我们证明了PSPACE-硬度验证的可预测性。
2020-02-13 cs.PL cs.SY eess.SY
Optimization-based Verification of Discrete-time Control Barrier Functions: A Branch-and-Bound Approach
Eindhoven University of Technology（埃因霍温理工大学）
本文提出一种受αBB算法启发的基于优化的分支定界方法，用于验证或证伪一般非线性离散时间系统的候选控制屏障函数，并通过数值案例验证其有效性。
2024-09-23 cs.SY eess.SY math.OC
Verification of Quantum Circuits through Discrete-Time Barrier Certificates
针对现有量子计算机验证多依赖定理证明器的问题，本文借鉴动态系统验证思路，提出复变量k归纳障碍证书方法，结合厄米特平方和优化计算，可用于验证多种量子电路的性质。
2024-08-14 cs.LO cs.SY eess.SY
Formal Verification of Robotic Contact Tasks via Reachability Analysis
Technical University of Munich（慕尼黑工业大学）
针对机器人接触任务中模型不确定性导致的验证难题，提出基于可达性分析的形式化验证方法，通过扩展混合动力学可达性分析并提出防护交集方法，成功验证了受限碰撞下的安全人机交互。
2023-07-26 cs.RO cs.SY eess.SY
On Prediction-Based Properties of Discrete-Event Systems: Notions, Applications and Supervisor Synthesis
针对部分可观测离散事件系统，提出基于预测的性质概念以建模依赖未来行为的性质，通过新型信息结构将监控器综合转化为信息空间安全博弈，得到可靠完备且最大允许的监控器综合算法。
2025-10-06 cs.SY eess.SY
On Epistemic Properties in Discrete-Event Systems: A Uniform Framework and Its Applications
提出面向部分可观测离散事件系统的双层观测者认知属性统一框架，可刻画高阶不透明性等知识推理，并给出系统化验证方法及高效可判定片段。
2024-09-10 cs.SY eess.SY
A unified concurrent-composition method to state/event inference and concealment in discrete-event systems
离散事件系统通常由离散状态和由标记（又名部分观察）事件的自发发生引起的离散状态之间的转换组成。由于部分观察到的特征，其中的基本属性可以分为两类：基于状态/事件推断的属性（例如，强的可检测性、可诊断性和可预测性）和基于状态隐藏的特性（例如，不透明度）。直觉上，前一类描述是否可以使用观察到的输出序列来推断当前和后续状态，过去发生的错误事件，或未来发生的错误事件;而后者描述是否不能使用观察到的输出序列来推断某些秘密状态是否已被访问（即DES是否可以隐藏其秘密状态已被访问的状态）。在过去的二十年里，这些属性分别使用不同的方法进行了研究。本文针对标号有限状态自动机，给出了一种统一的并发合成方法来验证上述基于推理的性质和基于隐藏的性质，从而为这两类性质建立了一个统一的数学框架。此外，与以往文献中的方法相比，并行合成方法不依赖于假设条件，效率更高。
2021-11-23 cs.CR cs.SY eess.SY
Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression
University of Colorado（科罗拉多大学）；TU Delft（代尔夫特理工大学）
本文提出一种基于高斯过程回归的形式化验证框架，用于从含噪数据中学习未知离散时间动力系统，并通过抽象为不确定马尔可夫决策过程及模型检查工具验证其满足时序逻辑规范，复杂度为多项式级。
2024-07-16 cs.AI cs.SY eess.SY
