DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2024.3

Execution-Time Opacity Problems in One-Clock Parametric Timed Automata

Authors: Étienne André, Johan Arcile, and Engel Lefaucheux

Published in: LIPIcs, Volume 323, 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)

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.

Cite as

Étienne André, Johan Arcile, and Engel Lefaucheux. Execution-Time Opacity Problems in One-Clock Parametric Timed Automata. In 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 323, pp. 3:1-3:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{andre_et_al:LIPIcs.FSTTCS.2024.3,
  author =	{Andr\'{e}, \'{E}tienne and Arcile, Johan and Lefaucheux, Engel},
  title =	{{Execution-Time Opacity Problems in One-Clock Parametric Timed Automata}},
  booktitle =	{44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024)},
  pages =	{3:1--3:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-355-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{323},
  editor =	{Barman, Siddharth and Lasota, S{\l}awomir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2024.3},
  URN =		{urn:nbn:de:0030-drops-221923},
  doi =		{10.4230/LIPIcs.FSTTCS.2024.3},
  annote =	{Keywords: Timed opacity, Parametric timed automata, Presburger arithmetic}
}

Search Results

Documents authored by Arcile, Johan

Execution-Time Opacity Problems in One-Clock Parametric Timed Automata

Abstract

Cite as

Thanks for your feedback!

Could not send message