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证明了时间不透明性问题——攻击者可观测带时间戳的动作并试图推断信息——对时间自动机是不可判定的。此外，他证明了即便对于事件记录自动机等子类，这一不可判定性仍然成立。本文采用相同的不透明性定义，通过限制系统或攻击者的能力进行研究。第一项贡献是证明了两种不透明性变体的相互可归约性：完全不透明性（无论是否访问私有位置，观测结果应完全一致）与弱不透明性（只需攻击者无法推断私有位置是否被访问，但允许推断其未被访问）；我们还进一步证明了包括与时间语言包含关系在内的关联性结果。第二项贡献是针对时间自动机的若干子类研究不透明性：包括对时钟数量、动作数量、时间性质（离散/连续）的限制，以及称为可观测事件记录自动机的新子类。研究表明，除单动作时间自动机和含ε-转换的单时钟时间自动机（仍保持不可判定性）外，不透明性在这些子类中基本可判定。第三项（可视为主要）贡献是提出不透明性的新定义，其中攻击者的观测次数被限制为前N次观测，或限制为N个时间戳集合（此后攻击者观测紧随其后的首个动作）。该集合既可先验定义，也可运行时定义；所有三种变体均使整个时间自动机类具有可判定性。