Title: New Insights into the Decidability of Opacity in Timed Automata Show Chinese title

Title: 时序自动机保密性的新见解

Abstract: This paper investigates the decidability of opacity in timed automata (TA), a property that has been proven to be undecidable in general. First, we address a theoretical gap in recent work by J. An et al. (FM 2024) by providing necessary and sufficient conditions for the decidability of location-based opacity in TA. Based on these conditions, we identify a new decidable subclass of TA, called timed automata with integer resets (IRTA), where clock resets are restricted to occurring at integer time points. We also present a verification algorithm for opacity in IRTA. On the other hand, we consider achieving decidable timed opacity by weakening the capabilities of intruders. Specifically, we show that opacity in general TA becomes decidable under the assumption that intruders can only observe time in discrete units. These results establish theoretical foundations for modeling timed systems and intruders in security analysis, enabling an effective balance between expressiveness and decidability. Show Chinese abstract

Abstract: 本文研究了时标自动机（TA）中透明性的可判定性问题，已知该性质在一般情况下是不可判定的。 首先，我们通过提供位置相关透明性在TA中的充分必要条件，解决了J. An等人（FM 2024）最近工作中存在的理论空白。 基于这些条件，我们识别出TA的一个新可判定子类，称为具有整数复位的时标自动机（IRTA），其中时钟复位被限制在整数时间点发生。 我们还提出了IRTA中透明性的验证算法。 另一方面，我们考虑通过削弱入侵者的功能来实现可判定的时间透明性。 具体来说，我们证明了在假设入侵者只能以离散单位观察时间的情况下，一般TA中的透明性变得可判定。 这些结果为安全分析中建模时标系统和入侵者建立了理论基础，能够在表达能力和可判定性之间实现有效的平衡。