Model Checking Differentially Private Properties.


Cited 14|Views48
No score
We introduce the branching time temporal logic Open image in new window for specifying differential privacy. Several differentially private mechanisms are formalized as Markov chains or Markov decision processes. Using our formal models, subtle privacy conditions are specified by Open image in new window . In order to verify privacy properties automatically, model checking problems are investigated. We give a model checking algorithm for Markov chains. Model checking Open image in new window properties on Markov decision processes however is shown to be undecidable.
Translated text
Key words
Model checking,Differential privacy,Temporal logic
AI Read Science
Must-Reading Tree
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined