Verification and synthesis for secrecy in discrete-event systems

Keeping a property of system behaviors secret from an observer (who has a partial observation of any executed behavior) requires that the execution of any property-satisfying or property-violating behavior must not become known to the observer. When an observer does not know the exact behaviors of a system it observes, a weaker notion of secrecy can be defined, which we introduce in this paper. We present an algorithm for verifying the properties of secrecy as well as its weaker version. When a given system does not possess a secrecy property, we consider restricting the behaviors of the system by means of supervisory control so as to ensure that the controlled system satisfies the desired secrecy property. We show the existence of a maximally permissive supervisor to ensure secrecy or its weaker version, and present algorithms for their synthesis.