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 RESTART. Villén-Altamirano recently showed—by way of a theoretical study and ad-hoc implementation—that a generalisation of RESTART to prolonged retrials offers improved performance. In this paper, we demonstrate our independent replication of the original experimental results. We implemented RESTART 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.
Replicating RESTART with Prolonged Retrials: An Experimental Report / Budde, Carlos E.; Hartmanns, Arnd. - ELETTRONICO. - 12652:(2021), pp. 373-380. (Intervento presentato al convegno TACAS 2021: 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems tenutosi a Luxembourg nel March 27 – April 1, 2021) [10.1007/978-3-030-72013-1_21].
Replicating RESTART with Prolonged Retrials: An Experimental Report
Carlos E. Budde;
2021-01-01
Abstract
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 RESTART. Villén-Altamirano recently showed—by way of a theoretical study and ad-hoc implementation—that a generalisation of RESTART to prolonged retrials offers improved performance. In this paper, we demonstrate our independent replication of the original experimental results. We implemented RESTART 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.File | Dimensione | Formato | |
---|---|---|---|
paper.pdf
accesso aperto
Descrizione: Article camera-ready
Tipologia:
Post-print referato (Refereed author’s manuscript)
Licenza:
Creative commons
Dimensione
523.77 kB
Formato
Adobe PDF
|
523.77 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione