%0 Conference Proceedings
%F atva09
%A Cassez, F.
%A Dubreil, J.
%A Marchand, H.
%T Dynamic Observers for the Synthesis of Opaque Systems
%B 7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09)
%E Liu, Z.
%E Ravn, A.P.
%V 	 5799
%P 352-367
%S LNCS
%I Springer-Verlag
%C Macao SAR, China
%X 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
%U http://www.irisa.fr/vertecs/Publis/Ps/atva09.pdf
%U http://dx.doi.org/10.1007/978-3-642-04761-9_26
%8 October
%D 2009