Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Evolution-Based Timed Opacity under a Universal Observation Model

Zhe Zhang, Martijn Goorden, Michel Reniers

Abstract

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.

Evolution-Based Timed Opacity under a Universal Observation Model

Abstract

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.

Paper Structure

This paper contains 16 sections, 11 theorems, 37 equations, 5 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. The Universal Observation Model
  4. Notion of EBTO
  5. Translation Between Opacity Notions
  6. Translation Between EBTO and LBTO
  7. Translation Between EBTO and ETO
  8. Conclusion
  9. Proofs
  10. Proof of Lemma \ref{['lem:YM_PY']}
  11. Proof of Lemma \ref{['lem:obs_equiv']}
  12. Proof of Theorem \ref{['app:thm:lbto_to_ebto']}
  13. Proof of Proposition \ref{['app:prop:ebto_to_lbto']}
  14. Proof of Lemma \ref{['lem:duration_strict']}
  15. Proof of Theorem \ref{['thm:eto_to_ebto']}
  16. ...and 1 more sections

Key Result

Theorem 1

Let $\mathcal{A}$ be a TA with SG $\mathcal{T}=\mathcal{S}(\mathcal{A})$, let $\Sigma_{\mathrm{obs}} \subseteq \Sigma$ be a given set of observable events where locations and clocks are unobservable (i.e., $L_{\mathrm{obs}} = \varnothing$ and $C_{\mathrm{obs}} = \varnothing$), and let $\mathcal{L}_s

Figures (5)

  • Figure 1: Semantically indistinguishable time-delay evolutions
  • Figure 2: A TA example illustrating suffix blindness.
  • Figure 3: The formal hierarchy of timed opacity classes.
  • Figure 4: The counter-example for suffix blindness: (a) shows the TA structure, and (b) illustrates states in the semantic graph. Blue states represent non-secret behaviors ($\tau \le \chi$), while red states represent secret behaviors ($\tau > \chi$).
  • Figure 5: Timed Automaton $\mathcal{A}$ illustrating path dependency on clock constraints.

Theorems & Definitions (28)

  • Definition 1: SG Rashidinejad2024
  • Definition 2: Observation mapping
  • Definition 3: Observational equivalence
  • Definition 4: EBTO
  • Definition 5: Mapping evolutions to timed words
  • Definition 6: Language-based timed opacity, LBTO An2025
  • Definition 7: Conversion function, LBTO to EBTO
  • Theorem 1: Sufficiency of EBTO for LBTO
  • Proposition 1: Strict expressiveness of EBTO over LBTO
  • Definition 8: ETO Andr2023
  • ...and 18 more