You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
41 lines
2.4 KiB
41 lines
2.4 KiB
Notes on the new approximate/statistical model checking support in PRISM
|
|
|
|
Previously, PRISM only supported a single kind of approximate/statistical model checking, namely checking of quantitative (e.g. P=?[...]) properties using the APMC method. Now, it offers four methods in total:
|
|
|
|
* CI (Confidence Interval)
|
|
* ACI (Asymptotic Confidence Interval)
|
|
* APMC (Approximate Probabilistic Model Checking)
|
|
* SPRT (Sequential Probability Ratio Test)
|
|
|
|
and these can also be applied to bounded (e.g. P<p[...]) properties. SPRT is only applicable to bounded properties. The default method used is CI (for quantitative properties) and SPRT for bounded properties.
|
|
|
|
Precise details of these methods can be found in the MSc thesis of Vincent Nimal:
|
|
http://www.prismmodelchecker.org/bibitem.php?key=Nim10
|
|
who worked on the code for this extension of PRISM.
|
|
|
|
A brief guide to enabling the various new options from the command-line is as follows.
|
|
(See also prism -help for a quick list.)
|
|
|
|
* Switch -sim means that any model checking is done using approximate/statistical methods.
|
|
|
|
* Switch -simmethod <name> selects the method to use: one of apmc, ci, aci, sprt.
|
|
The default is ci (Confidence Interval).
|
|
|
|
* These methods share several parameters, configurable as follows:
|
|
- simsamples <n> - sets the number of sample paths generated for CI/ACI/APMC
|
|
- simconf <x> - sets the confidence (a probability) for CI/ACI/APMC
|
|
- simwidth <x> - sets the (half)-width of the confidence interval for CI/ACI
|
|
- simapprox <x> - sets the approximation size for APMC
|
|
Each of CI/ACI/APMC has three parameters which are related so you can set at most two.
|
|
For APMC, the third parameter can be computed immediately; for CI/ACI, this is done after simulation.
|
|
SPRT has three parameters: the acceptable probability of Type I and II errors,
|
|
and the 'indifference' parameter. The first two are both set with -simconf, the third with -simwidth.
|
|
|
|
* Switch -simpathlen <n> sets the maximum length of paths generated by the simulator.
|
|
|
|
* Switches -simmanual, -simvar <n> and -simmaxrwd <x> refer to technical details
|
|
described in Vincent's thesis and can be ignored for now.
|
|
|
|
From the GUI, the mostly commonly used options can be set from the "Simulation Parameters"
|
|
which appears when performing approximate model checking.
|
|
The remaining options can be found in the "Simulator" tab of the "Options" dialog.
|