In decision-making problems, the actions of an agent may reveal sensitive information that drives its decisions. For instance, a corporation's investment decisions may reveal its sensitive knowledge about market dynamics. To prevent this type of information leakage, we introduce a policy synthesis algorithm that protects the privacy of the transition probabilities in a Markov decision process. We use differential privacy as the mathematical definition of privacy. The algorithm first perturbs the transition probabilities using a mechanism that provides differential privacy. Then, based on the privatized transition probabilities, we synthesize a policy using dynamic programming. Our main contribution is to bound the "cost of privacy," i.e., the difference between the expected total rewards with privacy and the expected total rewards without privacy. We also show that computing the cost of privacy has time complexity that is polynomial in the parameters of the problem. Moreover, we establish that the cost of privacy increases with the strength of differential privacy protections, and we quantify this increase. Finally, numerical experiments on two example environments validate the established relationship between the cost of privacy and the strength of data privacy protections.
We address the problem of synthesizing distorting mechanisms that maximize privacy of stochastic dynamical systems. Information about the system state is obtained through sensor measurements. This data is transmitted to a remote station through an unsecured/public communication network. We aim to keep part of the system state private (a private output); however, because the network is unsecured, adversaries might access sensor data and input signals, which can be used to estimate private outputs. To prevent an accurate estimation, we pass sensor data and input signals through a distorting (pri…
Data-driven systems are gathering increasing amounts of data from users, and sensitive user data requires privacy protections. In some cases, the data gathered is non-numerical or symbolic, and conventional approaches to privacy, e.g., adding noise, do not apply, though such systems still require privacy protections. Accordingly, we present a novel differential privacy framework for protecting trajectories generated by symbolic systems. These trajectories can be represented as words or strings over a finite alphabet. We develop new differential privacy mechanisms that approximate a sensitive w…
This paper investigates the problem of co-synthesis of edit function and supervisor for opacity enforcement in the supervisory control of discrete-event systems (DES), assuming the presence of an external (passive) intruder, where the following goals need to be achieved: 1) the external intruder should never infer the system secret, i.e., the system is opaque, and never be sure about the existence of the edit function, i.e., the edit function remains covert; 2) the controlled plant behaviors should satisfy some safety and nonblockingness requirements, in the presence of the edit function. We f…
In this work, we investigate the problem of privacy-preserving supervisory control against an external passive intruder via co-synthesis of dynamic mask, edit function, and supervisor for opacity enforcement and requirement satisfaction. We attempt to achieve the following goals: 1) the system secret cannot be inferred by the intruder, i.e., opacity of secrets against the intruder, and the existence of the dynamic mask and the edit function should not be discovered by the intruder, i.e., covertness of dynamic mask and edit function against the intruder; 2) the closed-loop system behaviors shou…
We study the synthesis of mode switching protocols for a class of discrete-time switched linear systems in which the mode jumps are governed by Markov decision processes (MDPs). We call such systems MDP-JLS for brevity. Each state of the MDP corresponds to a mode in the switched system. The probabilistic state transitions in the MDP represent the mode transitions. We focus on finding a policy that selects the switching actions at each mode such that the switched system that follows these actions is guaranteed to be stable. Given a policy in the MDP, the considered MDP-JLS reduces to a Markov j…
In this manuscript, we provide a set of tools (in terms of semidefinite programs) to synthesize Gaussian mechanisms to maximize privacy of databases. Information about the database is disclosed through queries requested by (potentially) adversarial users. We aim to keep part of the database private (private sensitive information); however, disclosed data could be used to estimate private information. To avoid an accurate estimation by the adversaries, we pass the requested data through distorting (privacy-preserving) mechanisms before transmission and send the distorted data to the user. These…
Multi-objective Robust Strategy Synthesis for Interval Markov Decision Processes
Saarland University（萨尔兰大学）；State Key Laboratory of Computer Science, ISCAS（中国科学院计算技术研究所）；Department of Computer Science, University of Oxford（牛津大学计算机系）
This work investigates the problem of analyzing privacy of abrupt changes for general Markov processes. These processes may be affected by changes, or exogenous signals, that need to remain private. Privacy refers to the disclosure of information of these changes through observations of the underlying Markov chain. In contrast to previous work on privacy, we study the problem for an online sequence of data. We use theoretical tools from optimal detection theory to motivate a definition of online privacy based on the average amount of information per observation of the stochastic system in cons…
In this paper, we investigate both qualitative and quantitative synthesis of optimal privacy-enforcing supervisors for partially-observed discrete-event systems. We consider a dynamic system whose information-flow is partially available to an intruder, which is modeled as a passive observer. We assume that the system has a "secret" that does not want to be revealed to the intruder. Our goal is to synthesize a supervisor that controls the system in a least-restrictive manner such that the closed-loop system meets the privacy requirement. For the qualitative case, we adopt the notion of infinite…
We present a method to find an optimal policy with respect to a reward function for a discounted Markov decision process under general linear temporal logic (LTL) specifications. Previous work has either focused on maximizing a cumulative reward objective under finite-duration tasks, specified by syntactically co-safe LTL, or maximizing an average reward for persistent (e.g., surveillance) tasks. This paper extends and generalizes these results by introducing a pair of occupancy measures to express the LTL satisfaction objective and the expected discounted reward objective, respectively. These…
Oden Institute for Computational Engineering and Sciences, University of Texas, Austin（奥斯汀德克萨斯大学奥登计算工程与科学研究所）；University of Florida（佛罗里达大学）
Privacy is an important concern in various multiagent systems in which data collected from the agents are sensitive. We propose a differentially private controller synthesis approach for multi-agent systems subject to high-level specifications expressed in metric temporal logic (MTL). We consider a setting where each agent sends data to a cloud (computing station) through a set of local hubs and the cloud is responsible for computing the control inputs of the agents. Specifically, each agent adds privacy noise (e.g., Gaussian noise) point-wise in time to its own outputs before sharing them wit…
In this paper, we propose a distributed differentially private receding horizon control (RHC) approach for multi-agent systems (MAS) with metric temporal logic (MTL) specifications. In the MAS considered in this paper, each agent privatizes its sensitive information from other agents using a differential privacy mechanism. In other words, each agent adds privacy noise (e.g., Gaussian noise) to its output to maintain its privacy and communicates its noisy output with its neighboring agents. We define two types of MTL specifications for the MAS: agent-level specifications and system-level specif…
Air Force Research Laboratory（空军研究实验室）；University of Central Florida（中佛罗里达大学）；University of Colorado Boulder（科罗拉多大学博尔德分校）
Given a Markov decision process (MDP) and a linear-time ($ω$-regular or LTL) specification, the controller synthesis problem aims to compute the optimal policy that satisfies the specification. More recently, problems that reason over the asymptotic behavior of systems have been proposed through the lens of steady-state planning. This entails finding a control policy for an MDP such that the Markov chain induced by the solution policy satisfies a given set of constraints on its steady-state distribution. This paper studies a generalization of the controller synthesis problem for a linear-time …
1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization
Technical University of Munich（慕尼黑工业大学）；Vali-e-Asr University of Rafsanjan（拉夫桑贾德瓦利阿斯尔大学）；Masaryk University（马萨里克大学）；Institute of Science and Technology（科学技术研究院）
