一句话：通过限制系统、攻击者及观测次数，证明时间自动机不透明性在多个子类与新定义下可判定。
时间自动机可建模带时钟的实时系统，但其时间不透明性在2009年被证明不可判定，事件记录自动机等子类亦如此。本文沿用同一不透明性定义，通过限制系统或攻击者研究可判定性。首先证明完全不透明性与弱不透明性可相互归约，并联系时间语言包含。其次分析时钟数、动作数、时间性质及新提出的可观测事件记录自动机等子类，发现多数情形可判定，但单动作时间自动机与带ε转移的单时钟时间自动机仍不可判定。最后提出仅允许攻击者观测前N次、或N个时间戳后首个动作的新定义，观测集可先验或运行时确定；三个版本均使整个时间自动机类可判定。
Timed automata (TAs) are an extension of finite automata that can measure and react to the passage of time, providing the ability to handle real-time constraints using clocks. In 2009, Franck Cassez showed that the timed opacity problem, where an attacker can observe some actions with their timestamps and attempts to deduce information, is undecidable for TAs. Moreover, he showed that the undecidability holds even for subclasses such as event-recording automata. In this article, we consider the same definition of opacity, by restricting either the system or the attacker. Our first contribution is to prove the inter-reducibility of two variants of opacity: full opacity (for which the observations should be the same regardless of the visit of a private location) and weak opacity (for which it suffices that the attacker cannot deduce whether the private location was visited, but for which it is harmless to deduce that it was not visited); we also prove further results including a connection with timed language inclusion. Our second contribution is to study opacity for several subclasses of TAs: with restrictions on the number of clocks, the number of actions, the nature of time, or a new subclass called observable event-recording automata. We show that opacity is mostly decidable in these cases, except for one-action TAs and for one-clock TAs with $ε$-transitions, for which undecidability remains. Our third (and arguably main) contribution is to propose a new definition of opacity in which the number of observations made by the attacker is limited to the first $N$ observations, or to a set of $N$ timestamps after which the attacker observes the first action that follows immediately. This set can be defined either a priori or at runtime; all three versions yield decidability for the whole TA class.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2408-12240,
title = {The Bright Side of Timed Opacity},
author = {Étienne André and Sarah Dépernet and Engel Lefaucheux},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 2},
year = {2026},
doi = {10.46298/lmcs-22(2:31)2026}
}