Replicating [Formula: see text] with Prolonged Retrials: An Experimental Report

Statistical model checking uses Monte Carlo simulation to analyse stochastic formal models. It avoids state space explosion, but requires rare event simulation techniques to efficiently estimate very low probabilities. One such technique is [Formula: see text] . Villén-Altamirano recently showed—by way of a theoretical study and ad-hoc implementation—that a generalisation of [Formula: see text] to prolonged retrials offers improved performance. In this paper, we demonstrate our independent replication of the original experimental results. We implemented [Formula: see text] with prolonged retrials in the and modes tools, and apply them to the models used originally. To do so, we had to resolve ambiguities in the original work, and refine our setup multiple times. We ultimately confirm the previous results, but our experience also highlights the need for precise documentation of experiments to enable replicability in computer science.