Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Execution-time opacity problems in one-clock parametric timed automata

Étienne André, Johan Arcile, Engel Lefaucheux

TL;DR

It is shown that the full ET-opacity emptiness is undecidable for a sufficiently large number of parameters, but is decidable for a single parameter, and exact synthesis can be effectively achieved.

Abstract

Parametric timed automata (PTAs) extend the concept of timed automata, by allowing timing delays not only specified by concrete values but also by parameters, allowing the analysis of systems with uncertainty regarding timing behaviors. The full execution-time opacity is defined as the problem in which an attacker must never be able to deduce whether some private location was visited, by only observing the execution time. The problem of full ET-opacity emptiness (i.e., the emptiness over the parameter valuations for which full execution-time opacity is satisfied) is known to be undecidable for general PTAs. We therefore focus here on one-clock PTAs with integer-valued parameters over dense time. We show that the full ET-opacity emptiness is undecidable for a sufficiently large number of parameters, but is decidable for a single parameter, and exact synthesis can be effectively achieved. Our proofs rely on a novel construction as well as on variants of Presburger arithmetics. We finally prove an additional decidability result on an existential variant of execution-time opacity.

Execution-time opacity problems in one-clock parametric timed automata

TL;DR

It is shown that the full ET-opacity emptiness is undecidable for a sufficiently large number of parameters, but is decidable for a single parameter, and exact synthesis can be effectively achieved.

Abstract

Parametric timed automata (PTAs) extend the concept of timed automata, by allowing timing delays not only specified by concrete values but also by parameters, allowing the analysis of systems with uncertainty regarding timing behaviors. The full execution-time opacity is defined as the problem in which an attacker must never be able to deduce whether some private location was visited, by only observing the execution time. The problem of full ET-opacity emptiness (i.e., the emptiness over the parameter valuations for which full execution-time opacity is satisfied) is known to be undecidable for general PTAs. We therefore focus here on one-clock PTAs with integer-valued parameters over dense time. We show that the full ET-opacity emptiness is undecidable for a sufficiently large number of parameters, but is decidable for a single parameter, and exact synthesis can be effectively achieved. Our proofs rely on a novel construction as well as on variants of Presburger arithmetics. We finally prove an additional decidability result on an existential variant of execution-time opacity.
Paper Structure (33 sections, 20 theorems, 9 equations, 3 figures, 1 table)

This paper contains 33 sections, 20 theorems, 9 equations, 3 figures, 1 table.

Table of Contents

  1. Introduction
  2. Contributions
  3. Related works
  4. Preliminaries
  5. Parametric timed automata
  6. Reachability synthesis
  7. Execution-time opacity problems ALLMS23
  8. A parametric execution times-based semi-algorithm for $\texttt{$\exists$OS}$ and $\texttt{FOS}$
  9. Parametric execution times
  10. Partial solution
  11. $\texttt{$\exists$OS}$ and $\texttt{FOS}$ problems
  12. On correctness and termination
  13. Decidability and undecidability of $\texttt{FOE}$ for 1-clock-PTAs
  14. Encoding infinite PET for $(1, 0, *)$-PTAs
  15. Defining the set of reset-free PTAs
  16. ...and 18 more sections

Key Result

Proposition 1

Let $\mathcal{A}$ be a PTA, and $\mathrm{\mathrm{\ell}_f}$ the final location of $\mathcal{A}$. Let $\mathcal{A}'$ be a copy of $\mathcal{A}$s.t.: Then, $\mathit{PET}(\mathcal{A}) = \textsf{EFsynth}(\mathcal{A}', \{\mathrm{\mathrm{\ell}_f}\})$.

Figures (3)

  • Figure 1: A PTA example and its transformed versions. The yellow dotted location is urgent.
  • Figure 2: A 1-clock PTA and the PET problem.
  • Figure 3: Reset-free automata of $\mathcal{A}$ (from \ref{['figure:1-clock_pta:pta']}) and automaton of the zones $\hat{\mathcal{A}}$.

Theorems & Definitions (53)

  • Definition 1: PTA AHV93
  • Definition 2: Reset-free PTA
  • Example 1
  • Definition 3: Semantics of a ta
  • Definition 4: Symbolic state
  • Definition 5: Symbolic semantics
  • Definition 6: *opacity for $D$
  • Definition 7: $\exists$-*opacity
  • Definition 8: full *opacity
  • Example 2
  • ...and 43 more