Confluence versus Partial Order Reduction in Statistical Model Checking and Simulation

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 the
first 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.