Avoiding event explosion when simulating PRISM models

The PRISM modeling language makes it possible to write very compact specifications of large discrete event systems. State variables provide you with the means to specify a factored state space, while modules and commands enable you to factor events into a compact representation. As an example, consider the following PRISM model for Herman's self stabilizing algorithm:

dtmc

const double p = 0.5;

module process1
  x1 : [0..1];

  [step]  (x1=x3) -> p : (x1'=0) + 1-p : (x1'=1);
  [step] !(x1=x3) -> (x1'=x3);
endmodule

module process2 = process1 [ x1=x2, x3=x1 ] endmodule
module process3 = process1 [ x1=x3, x3=x2 ] endmodule

This particular model has 8 states and 8 events. If we generalize from 3 to n modules, there are 2ⁿ states and events. In other words, this model exhibits both state and event explosion with a linear increase in the size of the specification. The event explosion is due to synchronizing commands. Every command has the same action label. When composing two modules, every combination of synchronizing commands must be considered.

Simulation-based methods for probabilistic model checking, such as those implemented in my own model checker Ymer, are often advertised as immune to state space explosion. Ymer does not generate an explicit-state model, and can simulate a PRISM model using the factored state representation inherent in the model specification. Ever since the first version of Ymer, however, I have always performed module composition explicitly prior to model simulation. This makes Ymer susceptible to the event explosion problem.

The limitation of Ymer with respect to event explosion is not a limitation of simulation-based methods in general. In fact, the simulation engine in PRISM (at least as of version 4.0) avoids this problem by performing on-demand model composition. If you look at the example model above, you might note that only one command of each module can be enable in any state. With on-demand model composition, you would consider only enabled commands for composition, so for the example model you go from evaluating the preconditions of 2ⁿ composed commands, to evaluating the preconditions of 2n module commands. In both cases, you end up with a single enabled composed command in any given state, but the reduced complexity of on-demand model composition is remarkable.

Preliminary results with a bare-bones simulator for PRISM models that implements on-demand module composition are promising (part of my effort to rewrite Ymer from scratch).