Dynamic Observers for the Synthesis of Opaque Systems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2009

Dynamic Observers for the Synthesis of Opaque Systems

Résumé

In this paper, we address the problem of synthesizing opaque systems. A secret predicate S over the runs of a system G is opaque to an external user having partial observability over G, if s/he can never infer from the observation of a run of G that the run belongs to S. We first investigate the case of static partial observability where the set of events the user can observe is fixed a priori. In this context, we show that checking whether a system is opaque is PSPACE-complete, which implies that computing an optimal static observer ensuring opacity is also a PSPACE-complete problem. Next, we introduce dynamic partial observability where the set of events the user can observe changes over time. We show how to check that a system is opaque w.r.t. to a dynamic observer and also address the corresponding synthesis problem: given a system G and secret states S, compute the set of dynamic observers under which S is opaque. Our main result is that the set of such observers can be finitely represented and can be computed in EXPTIME.
Fichier principal
Vignette du fichier
PI-1930.pdf (604.14 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00396442 , version 1 (18-06-2009)

Identifiants

  • HAL Id : inria-00396442 , version 1

Citer

Franck Cassez, Jérémy Dubreil, Hervé Marchand. Dynamic Observers for the Synthesis of Opaque Systems. [Research Report] PI 1930, 2009, pp.22. ⟨inria-00396442⟩
208 Consultations
266 Téléchargements

Partager

Gmail Facebook X LinkedIn More