Comparing the Notions of Opacity for Discrete-Event Systems
不透明度是一种信息流特性，它表征了一个系统是否会向被动的观察者揭示它的秘密。在文献中已经引入了几个不透明度的概念。我们研究了基于语言的不透明度，当前状态不透明度，初始状态不透明度，初始和最终状态不透明度，K步不透明度和无限步不透明度的概念。比较这些概念是一个自然的问题，Wu和Lafortune对此进行了研究和总结，他们提供了当前状态不透明性、初始和最终状态不透明性和基于语言的不透明性之间的转换，对于前缀封闭的语言，还提供了基于语言的不透明性和初始状态不透明性之间的转换。我们扩展这些结果表明，所有讨论的概念的不透明度是相互转化。除了更深入地了解概念之间的差异外，变换还可以应用于复杂性结果。特别是，变换是可计算的多项式时间，并保持可观察的事件和确定性的数量，因此计算复杂性的验证的概念相吻合。我们提供了一个完整的和改进的复杂性图片所讨论的概念的不透明度的验证，并提高算法的复杂性，决定基于语言的不透明度，无限步不透明度，和K步不透明度。
2021-06-26 cs.FL cs.SY eess.SY
Verification of Initial-State Opacity for Switched Systems: A Compositional Approach
信息流的安全性已经成为网络物理系统（CPS）的主要关注点。在这项工作中，我们专注于分析的信息流的安全属性，称为不透明性。不透明性的特点是在存在恶意外部入侵者的情况下，系统秘密的合理否认性。我们提出了一种方法来检查的概念不透明度，称为近似初始状态不透明度，离散时间切换系统的网络。我们的框架依赖于组合结构的有限抽象的网络切换系统和他们所谓的近似初始状态不透明度保持模拟功能（InitSOPSFs）。这些函数表征了具体网络及其有限抽象在满足近似初始状态不透明度方面的接近程度。我们表明，这样的InitSOPSFS可以通过假设一些小增益类型的条件和组成所谓的本地InitSOPSFS分别为每个子系统构建的组成。此外，假设切换系统具有一定的稳定性，我们还提供了一种技术来构建其有限抽象与相应的本地InitSOPSF。最后，我们通过一个例子来说明我们的结果的有效性。
2020-06-30 cs.SY eess.SY
Decentralized State Estimation and Opacity Verification Based on Partially Ordered Observation Sequences
本文研究分散式观测架构下的离散事件系统状态估计与不透明性验证，提出CSS结构以降低复杂度，并构建估计器验证初始状态及同步时当前状态不透明性。
2025-08-15 cs.SY eess.SY
Verification of Approximate Opacity via Barrier Certificates
本文的动机是越来越多的网络物理系统的安全问题。在这里，我们开发了一个无离散化的验证计划，目标是信息流的安全属性，称为近似初始状态不透明性，离散时间控制系统的类。我们提出了所谓的增强控制屏障证书的概念，并结合捕获系统初始集和秘密集的指定感兴趣区域。基于所提出的屏障证书的存在性，给出了离散时间控制系统（缺乏）近似初始状态不透明性的充分条件.我们进一步提出了一个有效的计算方法，铸造的条件为障碍证书的平方和规划问题。通过两个数值例子说明了所提出的结果的有效性。
2021-09-22 cs.SY eess.SY math.OC
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
Existential Opacity for Discrete-Event Systems with State Observations
The Hong Kong University of Science and Technology (Guangzhou)（香港科技大学（广州））
针对现有基于状态观测的不透明性无法捕捉部分场景需求的问题，提出存在性不透明性（EO）概念，其更具表达力，还开发了对应验证方法，为不透明性保护问题可行性提供新准则。
2026-09-03 cs.SY eess.SY
Verifying Weak and Strong k-Step Opacity in Discrete-Event Systems
本文针对离散事件系统，提出验证弱和强 k 步不透明性的新算法，其复杂度低于现有算法且不依赖于参数 k，通过将强归约为弱实现验证。
2023-05-15 cs.SY eess.SY
Secure Your Intention: On Notions of Pre-Opacity in Discrete-Event Systems
本文研究了部分可观测离散事件系统中一个重要的信息流安全性质--不透明性。我们认为存在一个被动的入侵者（窃听者），知道系统的动态模型，并可以使用生成的信息流来推断系统的一些“秘密”。如果一个系统总是对它的秘密持有合理的可否认性，那么它就被称为不透明的。现有的不透明性概念仅将秘密视为当前访问某些秘密状态或过去访问过某些秘密状态。在本文中，我们从一个新的角度来研究信息流的安全性，认为系统的秘密是在未来执行一些特定的重要行为的意图。为此，我们提出了一类新的不透明度称为前不透明度，其特征在于入侵者是否可以预测访问的秘密状态的一定数量的步骤之前，系统实际上这样做。根据入侵者的预测任务，我们提出了两种特定的预不透明度称为K步即时预不透明度和K步轨迹预不透明度来指定这个概念。对于每一个预不透明的概念，我们提供了一个必要和充分条件，以及一个有效的验证算法。验证预不透明度的复杂性是指数的系统的大小，因为我们表明，预不透明度是固有的PSPACE硬。最后，我们将我们的设置推广到系统的秘密意图被建模为执行特定的事件序列而不是访问秘密状态的情况。
2020-10-27 cs.SY eess.SY
You Don't Know What I Know: On Notion of High-Order Opacity in Discrete-Event Systems
本文研究了部分可观测离散事件系统中一类称为不透明性的信息流安全性质。粗略地说，一个系统被称为不透明的，如果入侵者，这是一个被动的观察者建模，永远不能确定的“秘密”的系统。大多数现有的不透明性概念考虑与系统的实际行为相关的秘密。在本文中，我们考虑了一种新的类型的秘密有关的知识的系统用户。具体来说，我们假设系统用户也只有部分的观察系统，并有理由的实际行为的系统。我们说一个系统是高阶不透明的，如果入侵者永远不能确定系统用户知道一些重要的信息，根据自己的不可比信息。给出了高阶不透明度的形式定义。两个算法提供了这个新的概念的验证：一个与双指数的复杂性的最坏情况下，另一个与单指数的复杂性。说明性的例子提供了高阶不透明度的新概念。
2022-03-31 cs.SY eess.SY
Opacity of Discrete Event Systems with Active Intruder
不透明度是一种安全属性，它形式化地描述了系统对外部观察者（即入侵者）的信息泄漏。离散事件系统（DES）文献中研究的传统不透明性通常假设被动入侵者，他们只观察系统的行为。然而，在许多网络安全问题，如Web服务，主动入侵者，谁能够影响系统的行为超出被动的观察，需要考虑和防御。因此，我们有动机扩展不透明的概念来处理主动入侵者。为此，我们将系统建模为非确定性有限状态换能器。假设入侵者对系统结构有充分的了解，并且能够通过注入不同的输入并观察其响应来与系统进行交互。在这种设置中，我们首先引入反应性当前状态不透明度（RCSO）的概念，其特征在于系统不泄漏其秘密状态，无论入侵者如何操纵系统的行为。我们进一步扩展这个概念，以语言为基础的和初始状态的反应不透明的概念，并研究它们之间的关系。结果表明，所有提出的反应不透明度概念都等价于RCSO。因此，我们专注于RCSO和研究其验证问题。它表明，RCSO可以通过构造一个观察者自动机进行验证。
2020-07-24 cs.LO cs.SY eess.SY
Generalized Current-State Opacity With Dynamically Changing Secrets
不透明度是一种与系统的隐私和安全性相关的信息流属性，在离散事件系统中得到了广泛的研究。虽然已经提出了各种不透明的概念，但在所有情况下，所考虑的秘密都是恒定的。这项工作的重点是当前状态的不透明性，考虑的情况下，秘密动态变化的系统演化。换句话说，我们提出了广义当前状态不透明度（GCSO）的新概念，这是相对于一个动态的秘密模型，而不是一个常数秘密。此外，我们提供了一种方法来验证GCSO的基础上的GCSO验证器的建设。最后，给出了一个实例来说明所提出的概念及其验证方法。
2021-02-27 cs.SY eess.SY
On Algorithms verifying Initial-and-Final-State Opacity: Complexity, Special Cases, and Comparison
本文研究了初始-终态不透明性（IFO）的验证算法，分析了基于网格状态估计器和语言包含归约的两种超指数复杂度算法，探讨了时间复杂度下界并通过基准测试进行了比较。
2024-12-24 cs.FL cs.SY eess.SY
Verification of Hyperproperties for Uncertain Dynamical Systems via Barrier Certificates
超属性是需要对系统的多个执行跟踪进行量化的系统属性。超属性可以表达信息物理系统的几个感兴趣的规范-例如不透明性，鲁棒性和非干扰性-这些都不能用线性时间属性来表达。本文首次提出了一种离散时间不确定动力系统超性质形式化验证的方法。所提出的方法涉及到复杂的hyperproperties分解成几个验证条件，利用基于自动机的结构对应的补充原始规范。这些验证条件然后通过合成所谓的增强屏障证书来解除，增强屏障证书为底层系统提供某些安全保证。对于系统的多项式型动态，我们提出了一个健全的程序来合成多项式型增强屏障证书减少问题的平方和优化。我们证明了我们提出的方法对两个重要的超性质：初始状态不透明性和初始状态鲁棒性的两个物理案例研究的有效性。
2021-11-23 cs.SY eess.SY
New Insights into the Decidability of Opacity in Timed Automata
School of Computer Science and Engineering, Sun Yat-Sen University（中山大学计算机科学与工程学院）
本文研究时间自动机不透明性的可判定性，通过提供充分必要条件识别出新的可判定子类IRTA并给出验证算法，同时证明在入侵者仅能离散观察时间的假设下一般TA的不透明性也可判定，为安全分析奠定理论基础。
2025-04-01 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
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
Estimation and Verification of Partially-Observed Discrete-Event Systems
Department of Automation, Shanghai Jiao Tong University（上海交通大学自动化系）
本文研究了离散事件系统在状态估计和验证中的问题，采用新的方法提高了系统的可靠性和安全性。
2019-03-27 cs.SY eess.SY
On Approximate Opacity of Cyber-Physical Systems
Shanghai Jiao Tong University（上海交通大学）；University of Colorado Boulder（科罗拉多大学博尔德分校）
本文研究了网络物理系统中近似不透明性的概念，提出了一种新的方法来评估系统在入侵者测量精度下的安全保证水平，并讨论了如何构建近似不透明性保持的符号模型。
2019-02-25 cs.SY eess.SY
Opacity Enforcement by Edit Functions Under Incomparable Observations
本文研究在入侵者与防御者观测能力不可比的离散事件系统中，通过编辑函数操纵输出观测来强制 opacity，提出 ic-enforceability 概念并将问题转化为不完全信息双人博弈，进而综合出可行的编辑函数。
2025-05-09 cs.FL cs.SY eess.SY
Finite-time Safety and Reach-avoid Verification of Stochastic Discrete-time Systems
Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；Key Laboratory of System Software (Chinese Academy of Sciences)（系统软件重点实验室（中国科学院））；State Key Laboratory of Computer Science（计算机科学技术国家重点实验室）
针对随机离散时间系统，本文提出新型类障碍充分条件以刻画有限时间安全性与到达规避概率的上下界，并通过两个示例验证其有效性。
2025-10-21 cs.SY eess.SY
Reachability Verification for Stochastic Discrete-time Dynamical Systems
本文研究了无限时域上随机离散动力系统的可达性验证问题。本文所研究的可达性验证是证明系统从一个指定的初始集合出发，最终进入一个期望的目标集合的可达概率的上、下界。基于Doob的非上鞅不等式，建立了无限时间范围内可达性验证的现有充分条件，这些条件通常是限制性的。最近，在[18]中提出了一组方程，其解能够表征精确的可达概率。受这一结果的启发，本文提出了基于放松此方程的可达性验证的充分条件。这些充分条件被证明是弱于国家的最先进的，因此能够提供更多的机会，成功地验证的可达性。
2023-02-20 cs.SY eess.SY
Comparative Analysis of Barrier-like Function Methods for Reach-Avoid Verification in Stochastic Discrete-Time Systems
University of Chinese Academy of Sciences（中国科学院大学）；East China Normal University（华东师范大学）；Nanyang Technological University（南洋理工大学）；Singapore Management University（新加坡管理大学）
本文比较了随机离散时间系统中多种屏障状函数方法，分析了它们的理论性质和计算可行性，并通过实验评估了实际性能。
2025-12-05 cs.SY eess.SY
Notions of Centralized and Decentralized Opacity in Linear Systems
University of Maryland, College Park（马里兰大学帕克分校）
本文研究了线性系统中集中式和去中心化不透明性的概念，提出了一种基于可达状态集的必要和充分条件，以确保秘密规范的k-ISO，并扩展了单对手系统的不透明性理论到多对手情况，同时考虑了集中协调器的存在与否以及对手之间的合谋情况。
2019-03-16 cs.CR 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
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
Sufficient and Necessary Barrier-like Conditions for Safety and Reach-avoid Verification of Stochastic Discrete-time Systems
Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所，系统软件重点实验室，计算机科学与技术国家重点实验室）
本文提出随机离散时间系统安全性和可达-回避验证的必要和充分屏障条件，通过放松贝尔曼方程建立必要性和充分性，解决无限时间 horizon 的安全性和可达-回避验证问题。
2026-01-05 cs.SY eess.SY
Verification of Quantum Circuits through Discrete-Time Barrier Certificates
针对现有量子计算机验证多依赖定理证明器的问题，本文借鉴动态系统验证思路，提出复变量k归纳障碍证书方法，结合厄米特平方和优化计算，可用于验证多种量子电路的性质。
2024-08-14 cs.LO cs.SY eess.SY
Quantitative Verification of Constrained Occupation Time for Stochastic Discrete-time Systems
KLSS, Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；Software Engineering Institute, East China Normal University（华东师范大学软件学院）；College of Computing and Data Science, Nanyang Technological University（南洋理工大学计算与数据科学学院）
本文提出首个能验证随机离散时间系统中目标集至少访问k次且保持安全的概率框架，通过乘法随机屏障函数和切换系统重构，推导了有限和无限时间 horizon 的严格概率界。
2026-04-20 cs.SY eess.SY
On Verification of D-Detectability for Discrete Event Systems
可检测性是离散事件系统状态估计性质的推广。它询问系统的当前和后续状态是否可以基于观察来确定。由于在某些应用中，精确地确定当前和后续状态可能过于严格，因此引入了D-可检测性的宽松概念，仅区分某些状态对而不是所有状态。定义了四种D-可探测性：强（周期性）D-可探测性和弱（周期性）D-可探测性。判定弱（周期性）D-可检测性是PSpace完备的，而判定强（周期性）可检测性或强D-可检测性是多项式的（我们证明了它实际上是NL完备的）。然而，据我们所知，这是一个开放的问题，是否存在一个多项式时间算法决定强周期D-可检测性。我们解决这个问题，决定强周期性的D-可检测性是一个PSpace完全的问题，因此没有多项式时间算法，除非PSpace = P.我们进一步表明，没有多项式时间算法决定强周期性的D-可检测性，即使是一个单一的可观察事件的系统，除非P = NP。最后，我们提出了一类系统的问题是易处理的。
2020-05-16 cs.FL cs.SY eess.SY
Opacity Enforcing Supervisory Control with a Priori Unknown Supervisors
Shanghai Jiao Tong University（上海交通大学）；Key Laboratory of System Control and Information Processing, the Ministry of Education of China（教育部系统控制与信息处理重点实验室）；Xidian University（西安电子科技大学）；University of Cagliari（卡利亚里大学）
本文研究了通过监督控制在离散事件系统中强制 opacity 的问题，提出了一种新的中间信息设置，即事先未知监督器设置，并设计了无约束的合成算法。
2026-04-05 cs.SY eess.SY
Optimal Synthesis of Opacity-Enforcing Supervisors for Qualitative and Quantitative Specifications
在本文中，我们研究了定性和定量合成的最优隐私执行监督的部分可观察离散事件系统。我们考虑一个动态系统的信息流是部分可用的入侵者，这是建模为一个被动的观察者。我们假设系统有一个“秘密”，不想透露给入侵者。我们的目标是合成一个监督者，以最少的限制方式控制系统，使闭环系统满足隐私要求。对于定性的情况下，我们采用无限步不透明的概念作为隐私规范，要求入侵者永远不能确定系统是/是在任何特定的时刻处于秘密状态。如果定性综合问题是不可解的或综合的解决方案是过于限制，那么我们进一步研究的定量综合问题，使秘密是揭示（如果不可避免的）尽可能晚。给出了解决定性和定量综合问题的有效算法。具体来说，通过建立适当的信息结构，涉及信息延迟，我们表明，最佳的定性综合问题可以解决的安全游戏。最优定量综合问题也可以作为一个增广信息结构上的最优总成本控制问题来解决。我们的工作提供了一个完整的解决方案，标准的无限步不透明度控制问题，这还没有得到解决，如果没有可控事件和可观测事件之间的关系的假设。此外，我们通过引入秘密揭示时间作为一种新的定量度量，将不透明性实施问题推广到数值环境。
2021-02-02 cs.SY eess.SY
A New Approach for Verification of Delay Coobservability of Discrete-Event Systems
在离散事件系统的分散网络监督控制中，本地监督者通过观察具有观测延迟的事件发生情况来做出正确的控制决策。延迟协同可观测性描述了这些局部监督者是否能够进行足够的观测。在本文中，我们提供了一个有效的方法来验证延迟可观测性。对于每个可控事件，我们划分的规范语言成有限数量的集合，使字符串在不同的集合有不同的长度。对于每个集合，我们构造一个验证器来检查可控事件的延迟可共观性是否成立。所提出的方法的计算复杂度是多项式的状态数，事件数，和上界的观察延迟和本地监督员的数量只指数。它具有较低的复杂性顺序比现有的方法。此外，我们还研究了网络化离散事件系统的分散监督控制与分散故障诊断之间的关系，证明了延迟$K$ -可诊断性可转化为延迟可观测性.因此，可以利用用于验证延迟协同可观测性的技术来验证延迟$K$协同可诊断性。
2022-05-19 cs.SY eess.SY
Sufficient and Necessary Continuous Barrier-like Conditions for Discrete-Time Stochastic Reach-Avoid Verification
ios.ac.cn（中国科学院自动化研究所）
本文针对离散时间随机系统无限时域可达-避让验证，提出基于连续障碍函数的充要条件，并利用SOS和SDP方法实现多项式障碍函数的综合，同时保证方法的可靠性与完备性。
2026-09-22 cs.SY eess.SY
Verification and Synthesis of Discrete-Time Control Barrier Functions
Eindhoven University of Technology（埃因霍温理工大学）
本文针对离散时间非线性系统，提出基于分支定界的DTCBF验证方法和基于双层优化的DTCBF与控制策略综合方法，并给出有限时间收敛性保证。
2025-09-23 cs.SY eess.SY math.OC
HyperCertificates: Verification of Discrete-time Dynamical Systems against HyperLTL Specifications
University of Colorado Boulder（科罗拉多大学博尔德分校）
本文提出一种归纳框架，通过超证书概念验证离散时间动态系统 against 超LTL规范。方法结合前瞻函数与屏障函数，利用闭包证书和SOS/SMT技术实现自动验证。
2026-05-01 cs.LO 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
Stochastic Stability Analysis of Discrete Time System Using Lyapunov Measure
Iowa State University（爱荷华州立大学）
本文研究了随机非线性离散时间系统的稳定性问题，提出基于线性转移算子的李雅普诺夫度量作为稳定性验证工具，并建立了李雅普诺夫函数与度量之间的联系，通过双算子性质展示其对偶性，提出有限维近似方法和粗随机稳定性概念。
2016-03-08 cs.SY eess.SY math.DS
A Framework for Safe Probabilistic Invariance Verification of Stochastic Dynamical Systems
本文提出面向离散与连续时间随机动态系统的安全概率不变性验证框架，利用 Doob 非负超鞅不等式或方程松弛构建优化，并通过半定规划示例验证其有效性。
2024-08-03 cs.SY eess.SY
Characterization, Verification and Computation of Robust Controlled Invariants for Monotone Dynamical Systems
本文针对离散时间单调动力系统，基于偏序关系分类，提出鲁棒受控不变量的集合与轨迹表征，并给出验证与计算算法，示例证明其有效性。
2023-06-24 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
Co-Buchi Barrier Certificates for Discrete-time Dynamical Systems
University of Colorado Boulder（科罗拉多大学博尔德分校）
本文提出共Buchi障碍证书方法，用于验证离散时间动力系统在给定谓词上固定次数访问的性质，通过有界综合范式与LTL可实现性相结合，实现安全自动机转换和有效性验证。
2026-01-20 cs.FL 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
Verification of general Markov decision processes by approximate similarity relations and policy refinement
Eindhoven University of Technology（埃因霍温理工大学）；University of Oxford（牛津大学）
本文提出新的近似相似关系，用于在一般马尔可夫决策过程中进行策略合成，通过度量平衡概率分布偏差与模型输出距离，实现对抽象模型的控制细化。
2016-05-31 cs.SY eess.SY
Neural Contraction Metrics with Formal Guarantees for Discrete-Time Nonlinear Dynamical Systems
University of Illinois Urbana-Champaign (UIUC)（伊利诺伊大学厄巴纳-香槟分校）
本文提出一种学习神经网络收缩度量并利用α,β-CROWN验证器进行形式验证的方法，仅需动力学连续性假设，适用于离散时间非线性系统，并通过多个非线性示例验证了其有效性。
2025-04-23 cs.LG cs.SY eess.SY
A unified framework for modeling and implementation of hybrid systems with synchronous controllers
University of Auckland（奥克兰大学）
本文提出了一种新的方法，用于在线性混合自动机方法中包含非即时的离散控制转换。通过扩展同步子集的SystemJ编程语言，研究了如何用同步编程语言控制持续变化的模拟植物，并提供了一种合理的重写语义来近似连续变量在离散域中的演化。
2015-01-23 cs.PL cs.SY eess.SY
Complexity of Local Observation Consistency in Discrete-Event Systems
UPOL（奥洛穆茨大学）
本文研究离散事件系统中局部观测一致性（LOC）与局部重标注观测一致性（LROC）的复杂性，证明非确定性被控对象下二者为PSpace完全问题，确定性被控对象下可多项式时间判定，为相关控制应用提供理论依据。
2026-08-12 cs.SY eess.SY
