RML with importance sampling

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.


Importance sampling is implemented with the following algorithms:

  • Montecarlo
  • Chernoff
  • Chernoff ND

Comments are closed.