Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2603.26573 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917364561346560 |
|---|---|
| author | Zhang, Zhe Goorden, Martijn Reniers, Michel |
| author_facet | Zhang, Zhe Goorden, Martijn Reniers, Michel |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_26573 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Evolution-Based Timed Opacity under a Universal Observation Model Zhang, Zhe Goorden, Martijn Reniers, Michel Formal Languages and Automata Theory Cryptography and Security 93C65, 68Q45 F.1.1; F.4.3 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. |
| title | Evolution-Based Timed Opacity under a Universal Observation Model |
| topic | Formal Languages and Automata Theory Cryptography and Security 93C65, 68Q45 F.1.1; F.4.3 |
| url | https://arxiv.org/abs/2603.26573 |