Evolution-Based Timed Opacity under a Universal Observation Model

TL;DR

This paper introduces a unified framework for timed opacity in automata, using a universal observation model to compare different opacity variants and establish formal relationships.

Contribution

It proposes a universal observation model and defines evolution-based timed opacity, linking it to existing opacity notions and creating a unified semantic hierarchy.

Findings

Evolution-based timed opacity implies language-based timed opacity.

The framework establishes formal equivalences under constrained observations.

A semantic hierarchy for timed opacity is formally characterized.

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.