dpCTL Model Checker

After downloading the .zip file, first please refer to this page to build ePMC:wiki: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_{x}$$

to be continue…