Existing literature on timed opacity uses specific definitions for restricted subclasses of timed automata or limited observation models. This lack of a unified definition makes it difficult to establish formal relationships and compare the expressiveness of different opacity variants. This paper establishes a unified framework for timed opacity by introducing a universal observation model for timed automata. First, we introduce an observation model with full observation of time delay and partial observation of locations, clocks, and events. Second, based on this model, we define the notion of evolution-based timed opacity. Third, we mathematically prove that evolution-based timed opacity strictly implies language-based timed opacity and establish a formal equivalence with execution-time opacity under constrained observations. This framework establishes a unified semantic hierarchy for characterizing the landscape of timed opacity.
翻译:现有关于时间不透明性的文献针对时间自动机的受限子类或有限观测模型提出了特定定义。这种统一定义的缺失使得难以建立不同不透明性变体之间的形式化关系,并比较其表达能力。本文通过引入时间自动机的统一观测模型,建立了时间不透明性的统一框架。首先,我们提出了一种同时具备时间延迟完全观测与位置、时钟、事件部分观测的观测模型。其次,基于该模型定义了基于演化的时间不透明性概念。再次,通过数学证明,基于演化的时间不透明性严格蕴涵基于语言的时间不透明性,并在受限观测条件下建立了与执行时间不透明性的形式等价关系。该框架为描述时间不透明性的全景图建立了统一的语义层次结构。