定时离散事件系统不透明性验证的新突破：整数重置自动机与离散时间精度下的可判定性分析

《Automatica》：New insights into opacity verification in timed discrete-event systems

本文针对定时离散事件系统（TDES）中不透明性（opacity）验证这一核心安全问题展开研究。作者通过建立当前状态定时不透明性（CLTO）可判定性的充要条件，弥补了现有理论空白，并首次证明该属性在整数重置定时自动机（IRTA）子类中可判定且给出验证算法。创新性地引入离散时间精度入侵者模型（CLTO-IDTP），为一般定时自动机（TA）的不透明性分析提供了可判定框架，在系统表达力与计算可处理性间取得重要平衡。

　　

章节精选

预备知识

本节介绍后续讨论所需的符号和基本概念。令N={0,1,...}表示自然数集，[m:n]表示整数集{m,m+1,...,n}。R和R_≥0分别表示实数和非负实数集。我们用?d?、frac(d)和?d?分别表示d的整数部分、小数部分和最小上界整数。

定时不透明性可判定性的等价刻画

本节建立TA中CLTO可判定性的充要条件，并开发IRTA的CLTO验证算法。

离散时间精度入侵者下的定时不透明性

本节研究在入侵者仅能观测离散时间单位的假设下，一般TA的定时不透明性。大量定时不透明性研究隐含假设入侵者能进行任意精度的实值时钟测量，但实际应用中无需考虑如此强大的入侵者模型，因为现实时钟通常具有有限精度。因此，入侵者的实值时间读数可转换为离散观测。

结论

本文建立了TA中CLTO验证可判定的充要条件，从而完善了An等人（2024）先前报道的单独充分必要条件。利用这些条件结合IRTA现有成果，我们论证了IRTA的CLTO可判定性，并提出相应验证算法。此外，通过假设入侵者仅以离散单位观测时间，我们为一般TA开发了新的可判定框架。