Execution-time opacity problems in one-clock parametric timed automata - INRIA - Institut National de Recherche en Informatique et en Automatique
Conference Papers Year : 2024

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

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.
Fichier principal
Vignette du fichier
2410.01659v1.pdf (418.46 Ko) Télécharger le fichier
Origin Files produced by the author(s)

Dates and versions

hal-04732521 , version 1 (11-10-2024)

Licence

Identifiers

Cite

Étienne André, Johan Arcile, Engel Lefaucheux. Execution-time opacity problems in one-clock parametric timed automata. FSTTCS 2024, Dec 2024, Gandhinagar, India. ⟨hal-04732521⟩
62 View
8 Download

Altmetric

Share

More