Name
Abstract | ||
|---|---|---|
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. |
Year | Venue | Field |
|---|---|---|
2018 | APLAS | Model checking,Differential privacy,Computer science,Markov chain,Markov decision process,Theoretical computer science,Temporal logic,Undecidable problem,Branching (version control) |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
21 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Depeng Liu | 1 | 0 | 1.01 |
| Bow-Yaw Wang | 2 | 5 | 1.43 |
| Lijun Zhang | 3 | 245 | 37.10 |