Synthesis of Privacy-Preserving Systems

We introduce a framework for synthesis that addresses privacy of the system and its environment. In addition to a specification, the user provides a secret (both in terms of LTL formulas). We distinguish between two settings. In the first, values of some input and output signals are hidden from an observer in a way that respects budget constraints on the set of signals that may be hidden. In all environments, the specification should be satisfied and the value of the secret should be hidden from the observer. In the second setting, the system and the environment hide values of some signals from each other (technically, the generated transducer instructs the environment which input signals to assign in each round, and provides a partial assignment to the output signals). Here, in all environments, the specification should be satisfied with the incomplete information, and the satisfaction value of the secret should be hidden. 

Joint work with Ofer Leshkowitz and Naama Shamash-Halevy