release
Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision | ||
release [2020/11/17 01:12] – created conan | release [2020/11/18 19:30] (current) – [Simple case study] conan | ||
---|---|---|---|
Line 20: | Line 20: | ||
</ | </ | ||
- | In order to use our tool, a model file and a property file is request, following the standards of PRISM format([[http:// | + | In order to use our tool, a model file and a property file is request, following the standards of PRISM format([[http:// |
+ | and it will tell the model checker to check that for any initial states $s_1$ and $s_2$(assumed in neighborhood relations), whether | ||
+ | $Pr(s_1\models Pathformula) \le e^{\epsilon} Pr(s_2\models Pathformula) + \delta $ | ||
+ | |||
+ | holds. If there' | ||
+ | |||
+ | |||
+ | ==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' | ||
+ | [b] s=0 -> 0.8 : (s'=2) + 0.2 : (s' | ||
+ | [a] s=1 -> 0.25 : (s'=2) + 0.75 : (s' | ||
+ | [b] s=0 -> 0.2 : (s'=2) + 0.8 : (s' | ||
+ | endmodule | ||
+ | |||
+ | init s = 0 | s = 1 endinit | ||
+ | </ | ||
+ | |||
+ | The model is like this in the original paper[3]: | ||
+ | |||
+ | {{: | ||
+ | |||
+ | And the property file: | ||
+ | |||
+ | <code java> | ||
+ | e = 2.71828183 | ||
+ | D{log(3, | ||
+ | D{log(4, | ||
+ | </ | ||
+ | |||
+ | The second property with $\epsilon = \ln 4$ is the only one to be satisfied. | ||
release.1605546771.txt.gz · Last modified: 2020/11/17 01:12 (external edit)