Oct 11, 2012: Mark Timmer: Confluence versus Partial Order Reduction in Statistical Model Checking and Simulation

October 11, 2012Confluence versus Partial Order Reduction in Statistical Model Checking and Simulation
Room: Zi 4126Mark Timmer

Statistical model checking is an analysis method that circumvents the state space explosion problem in model-based verification, by combining probabilistic simulation with sequential hypothesis testing. As a simulation-based technique, it can only provide sound results if the underlying model is a stochastic process. In verification, however, models are usually variations of nondeterministic transition systems. One approach to extend the applicability of statistical model checking in this domain is to combine the simulative exploration with an on-the-fly check, based on partial order methods, to detect and discard spurious nondeterminism. In this presentation, we discuss an alternative that is based on the notion of confluence, which has recently been shown to be more powerful than partial order reduction. It considers only the concrete state space, without the need for independence conditions that can only feasibly be checked on a symbolic level. Therefore, confluence for thefirst time allows statistical model checking for models where the spurious nondeterminism does not only result from the interleaving of component behaviours. We compare the strength of the confluence and partial-order based approaches on a set of case studies and review the differences in performance, based on our implementation as part of the modes simulator for the Modest modelling language.