Simulation with memoryless distributions

Let X be a continuous random variable. The probability distribution of X is memoryless if Pr[X > t + s | X > t] = Pr[X > s]. The exponential distribution is the only memoryless continuous distribution. To see that the exponential distribution is indeed memoryless, recall that if X is exponentially distributed with rate λ, then Pr[X ≤ t] = 1 − e^−λt. We thus have Pr[X > t + s | X > t] = Pr[X > t + s and X > t] ÷ Pr[X > t] = Pr[X > t + s] ÷ Pr[X > t] = e^{−λ(t + s)} ÷ e^−λt = e^−λs = Pr[X > s].

Say we want to simulate a telephone exchange, with the assumption that the length of a phone call is exponentially distributed. When a phone call comes in, we sample a duration for the call from the exponential distribution. If the state of the system changes before the phone call ends, should we (i) subtract the elapsed time from the previously sampled duration or (ii) sample a new remaining duration from the original distribution as if the call had just started? For a memoryless distribution, it actually does not matter. This is exactly what the memoryless property tells us.

Early versions of Ymer (before version 3.0) used approach (i) as it treated the exponential distribution the same way as non-memoryless distributions. For non-memoryless distributions, you cannot sample a remaining duration from the original distribution, so instead you keep track of the originally sampled trigger times for events that remain enabled after state changes. Of course, if an event gets disabled before it triggers, you need to throw away the old trigger time, and sample a new trigger time when the event becomes enabled again. In later versions of Ymer, approach (ii) was adopted specifically for the exponential distribution as it reduces the amount of state that the simulator has to keep around and you do not have to check if an event with an exponential distribution was enabled in the previous state. This is also the approach implemented in the PRISM simulator. Ymer still uses approach (i) for non-memoryless distributions, for which PRISM currently lacks support.

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).