Differences

This shows you the differences between two versions of the page.

--- release [2020/11/17 01:13] – conan
+++ release [2020/11/18 19:30] (current) – [Simple case study] conan
@@ Line 20: / Line 20: @@
 </code>
-In order to use our tool, a model file and a property file is request, following the standards of PRISM format([[http://www.prismmodelchecker.org/manual/ThePRISMLanguage|ThePRISMLanguage]]). To specify the differentially private properties, a new operator <code bibtex> $$D_{x}$$</code>
+In order to use our tool, a model file and a property file is request, following the standards of PRISM format([[http://www.prismmodelchecker.org/manual/ThePRISMLanguage|ThePRISMLanguage]]). To specify the differentially private properties, a new operator  $D\{\epsilon,\delta\}[Pathformula]$ is introduced,
+and it will tell the model checker to check that for any initial states $s_1$ and $s_2$(assumed in neighborhood relations), whether
-to be continue...
+$Pr(s_1\models Pathformula) \le e^{\epsilon} Pr(s_2\models Pathformula) + \delta $
+holds. If there's a violation of the formula, differential privacy is not achieved and a counterexample of  $s_1$ and $s_2$, along with the probabilities will be given. Otherwise, the model checker returns an answer "yes". Examples of formulae are shown below:
+==D {3, 0} [F (1 < s & s <= 2) ]==
+==D {1, 0} [X ((d = -1) & (t = -1) )]==
+=====Simple case study=====
+Below are the model file(MDP) and property file of a survey mechanism with high/low accuracy.
+<code java>
+mdp
+module M1
+	// local state
+	s : [0..3] ;
+	[a] s=0 -> 0.75 : (s'=2) + 0.25 : (s'=3);
+	[b] s=0 -> 0.8 : (s'=2) + 0.2 : (s'=3);
+	[a] s=1 -> 0.25 : (s'=2) + 0.75 : (s'=3);
+	[b] s=0 -> 0.2 : (s'=2) + 0.8 : (s'=3);
+endmodule
+init s = 0  | s = 1 endinit
+</code>
+The model is like this in the original paper[3]:
+{{:1605697988.png?400|}}
+And the property file:
+<code java>
+e = 2.71828183
+D{log(3,e),0} [F (s=2 | s=3)]
+D{log(4,e),0} [F (s=2 | s=3)]
+</code>
+The second property with $\epsilon = \ln 4$ is the only one to be satisfied.