Synthesis of Privacy-Preserving Systems
=======================================

Synthesis is the automated construction of a system from its specification. In many cases, we want to maintain the privacy of the system and the environment, thus limit the information that they share with each other or with an observer of the interaction.
We introduce a framework for synthesis that addresses privacy in a simple yet powerful way. Our method is based on specification formalisms that include an unknown truth value. When the system and the environment interact, they may keep the truth values of some input and output signals private, which may cause the satisfaction value of specifications to become unknown. The input to the synthesis problem contains, in addition to the specification f, also  secrets g1,g2,...,gn. During the interaction, the system directs the environment which input signals should stay private. The system then realizes the specification if in all interactions, the satisfaction value of the specification f is true, whereas the satisfaction value of the secrets g1,g2,...,gn is unknown. Thus, the specification is satisfied without the secrets being revealed.
We describe our framework for specifications and secrets in LTL, and extend the framework also to the multi-valued specification formalism LTL[F], which enables the specification of the  quality of computations. When both the specification and secrets are in LTL[F], one can trade-off the satisfaction value of the specification with the extent to which the satisfaction values of the secrets are revealed. We show that the complexity of the problem in all settings is 2EXPTIME-complete, thus it is not harder than synthesis with no privacy requirements.