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.

翻译：定时自动机（TAs）是有限自动机的扩展，能够测量并响应时间流逝，利用时钟处理实时约束。2009年，Franck Cassez 证明了定时透明性问题（攻击者可观测带有时间戳的某些动作并试图推断信息）对于 TAs 是不可判定的。此外，他表明即使对于事件记录自动机等子类，该不可判定性依然成立。本文基于相同的透明度定义，通过限制系统或攻击者进行研究。第一个贡献是证明了透明性的两种变体之间的相互可归约性：完全透明性（其中无论是否访问私有位置，观测结果应相同）与弱透明性（只需攻击者无法推断私有位置是否被访问，但推断出未被访问是无害的）；我们进一步证明了包括与定时语言包含关系关联的其他结果。第二个贡献是研究了若干 TA 子类中的透明性：包括对时钟数量、动作数量、时间性质，以及名为“可观测事件记录自动机”的新子类的限制。研究表明，除含单动作 TA 和含 ε 转移的单时钟 TA 仍保持不可判定性外，多数情况下透明性是可判定的。第三个贡献（可视为主要贡献）是提出了一种新的透明性定义，其中攻击者的观测次数被限制为前 N 次观测，或针对一组 N 个时间戳（在此之后攻击者观测紧随其后的首个动作）。该集合可先验定义或在运行时定义；所有三种版本均使整个 TA 类获得可判定性。