New Insights into the Decidability of Opacity in Timed Automata

TL;DR

The paper addresses the decidability of opacity in timed automata (TA), highlighting undecidability in the general TA setting and proposing a complete characterization for location-based timed opacity (CLTO). It proves that CLTO is decidable for a TA subclass $\,\mathbb{X}$ if and only if the language-inclusion problem for $\,\epsilon$-$\mathbb{X}$ is decidable, and uses this to establish a new decidable subclass, timed automata with integer resets (IRTA), along with a CLTO verification algorithm. It also introduces CLTO-IDTP, a weaker notion where intruders observe time in discrete units, and provides a decidable verification method for it via closed timed region automata. Together, these results offer a principled framework for balancing expressiveness and decidability in security analyses of timed systems and point to future work on more scalable verification techniques.

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.

Figures (9)

• Figure 1: The IRTA $\mathcal{A}$ in Example \ref{['ex:1']}.
• Figure 2: The $\overline{\mathcal{A}_{\epsilon}}$ in Example \ref{['ex:1']}, where the invalid transitions are erased.
• Figure 3: The $\mathcal{R}(\overline{\mathcal{A}_{\epsilon}})$ in Example \ref{['ex:1']}, where "A","B","C","D" and "E" denote the regions of $[x=c=0]$, $[0<x=c<1]$, $[x=c=1]$, $[1 \leq x=c, \operatorname{frac}(c)=0]$ and $[1\leq x=c, \operatorname{frac}(c) > 0]$, respectively, and the unreachable states are erased.
• Figure 4: A part of $\mathscr{H}$ in Example \ref{['ex:1']}.
• Figure 5: The TA $\mathcal{A}$ in Example \ref{['ex:2']}.

Theorems & Definitions (26)

• Definition 1
• Definition 2
• Definition 3
• Definition 4
• Definition 5
• Proposition 1
• Proposition 2
• Claim 1
• Claim 2
• Theorem 1