Importance sampling allows to modify the parameters of a model in order to increase the probability of generating rare properties. From version 1.3.4 of PLASMA Lab we have included these sampling parameters in the RML language.
Model type
Importance sampling uses a different simulator in order to simulate the model according to the sampling parameters and to compute the modified rate of each run. This simulator is enable by using the keyword sampling after the model type. Therefore the following model types are available for importance sampling:
- dtmc sampling
- ctmc sampling
- mdp sampling
- mdp shd sampling
- mdp sml sampling
Sampling parameters
Two types of sampling parameters are available:
- command rates
- action rates
Command rates are declared with { expr } after the channel declaration. The effect is to specify a rate that increases or decreases the probability of firing this command.
Action rates are declared with { expr } before the normal rate of an action. This new rate replaces the normal rate of the action.
Algorithms
Importance sampling is implemented with the following algorithms:
- Montecarlo
- Chernoff
- Chernoff ND
