How to use the tool
After downloading the .zip file, first please refer to this page to build ePMC.
To perform dpCTL model checking, please set the following options:
--property-solver propositional-explicit,operator-explicit,pctl-explicit-next,dpctl-explicit-knowledge,dpctl-explicit-until
--prism-flatten false
--model-input-type mas
--property-input-type dpctl
--smtlib-command-line z3 -smt2 {0}
--smtlib-version v25
--constraintsolver-solver smt-lib
--model-input-files /path/to/your-model
--property-input-files /path/to/your-property
In order to use our tool, a model file and a property file is request, following the standards of PRISM format (ThePRISMLanguage). To specify the differentially private properties, a new operator D{ε,δ}[Pathformula] is introduced, and it will tell the model checker to check that for any initial states s1 and s2 (assumed in neighborhood relations), whether Pr(s1 |= Pathformula) ≤ eε Pr(s2 |= Pathformula) + δ holds. If there’s a violation of the formula, differential privacy is not achieved and a counterexample of s1 and s2, 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.
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
The model is like this in the original paper3:
And the property file:
e = 2.71828183
D {log(3,e), 0} [F (s=2 | s=3)]
D {log(4,e), 0} [F (s=2 | s=3)]
The second property with ε = ln 4 is the only one to be satisfied.