Automated Rare Event Simulation for Stochastic Petri Nets

We introduce a method to automatically apply rare event simulation to stochastic Petri nets, which are often used in the stochastic model checking community to model highly reliable systems. Rare event simulation can be much faster than standard simulation by exploiting information about the typical behaviour of the system. Previously, such information came from heuristics, human insight, or analysis on the full state space. We present a formal algorithm that obtains the required information from the (high-level) stochastic Petri net description, without generating the full state space. Essentially, our algorithm reduces the state space of the model to a (much smaller) graph in which each node represents a set of states for which the most likely path to failure has the same form. An earlier version of this work has been presented to the model checking commmunity (at QEST 2013). We believe that the described methodology, which has since then been improved through a correctness proof and a more efficient initial state space partitioning, may also be of interest to the RESIM community.