Replicating RESTART with Prolonged Retrials: An Experimental Report

Carlos E. Budde; Arnd Hartmanns

doi:10.1007/978-3-030-72013-1_21

Replicating RESTART with Prolonged Retrials: An Experimental Report

Carlos E. Budde^*, Arnd Hartmanns^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

15 Downloads (Pure)

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.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part I
Editors	Jan Friso Groote, Kim Guldstrand Larsen
Publisher	Springer
Pages	373-380
Number of pages	8
ISBN (Electronic)	978-3-030-72013-1
ISBN (Print)	978-3-030-72012-4
DOIs	https://doi.org/10.1007/978-3-030-72013-1_21
Publication status	Published - 23 Mar 2021
Event	27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021 - Online Event Duration: 27 Mar 2021 → 1 Apr 2021 Conference number: 27

Publication series

Name	Lecture Notes in Computer Science
Volume	LNCS 12652
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021
Abbreviated title	TACAS 2021
City	Online Event
Period	27/03/21 → 1/04/21
Other	Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021

Access to Document

10.1007/978-3-030-72013-1_21Licence: CC BY

10.1007_978-3-030-72013-1_21Final published version, 393 KBLicence: CC BY

Cite this

Budde, C. E., & Hartmanns, A. (2021). Replicating RESTART with Prolonged Retrials: An Experimental Report. In J. F. Groote, & K. Guldstrand Larsen (Eds.), Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part I (pp. 373-380). (Lecture Notes in Computer Science; Vol. LNCS 12652). Springer. https://doi.org/10.1007/978-3-030-72013-1_21

Budde, Carlos E. ; Hartmanns, Arnd. / Replicating RESTART with Prolonged Retrials: An Experimental Report. Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part I. editor / Jan Friso Groote ; Kim Guldstrand Larsen. Springer, 2021. pp. 373-380 (Lecture Notes in Computer Science).

@inbook{11d528ed485244a2bfa8c172bfcb9e46,

title = "Replicating RESTART with Prolonged Retrials: An Experimental Report",

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{\'e}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.",

author = "Budde, {Carlos E.} and Arnd Hartmanns",

year = "2021",

month = mar,

day = "23",

doi = "10.1007/978-3-030-72013-1_21",

language = "English",

isbn = "978-3-030-72012-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "373--380",

editor = "Groote, {Jan Friso} and {Guldstrand Larsen}, Kim",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part I",

address = "Netherlands",

note = "27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021, TACAS 2021 ; Conference date: 27-03-2021 Through 01-04-2021",

}

Budde, CE & Hartmanns, A 2021, Replicating RESTART with Prolonged Retrials: An Experimental Report. in JF Groote & K Guldstrand Larsen (eds), Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part I. Lecture Notes in Computer Science, vol. LNCS 12652, Springer, pp. 373-380, 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021, Online Event, 27/03/21. https://doi.org/10.1007/978-3-030-72013-1_21

Replicating RESTART with Prolonged Retrials: An Experimental Report. / Budde, Carlos E.; Hartmanns, Arnd.

Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part I. ed. / Jan Friso Groote; Kim Guldstrand Larsen. Springer, 2021. p. 373-380 (Lecture Notes in Computer Science; Vol. LNCS 12652).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

TY - CHAP

T1 - Replicating RESTART with Prolonged Retrials: An Experimental Report

AU - Budde, Carlos E.

AU - Hartmanns, Arnd

N1 - Conference code: 27

PY - 2021/3/23

Y1 - 2021/3/23

N2 - 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.

AB - 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.

UR - https://doi.org/10.1007/978-3-030-72013-1_21

UR - https://figshare.com/articles/software/Reproducing_RESTART_with_Prolonged_Retrials_An_Experimental_Report_experimental_replication_package_/12269462

U2 - 10.1007/978-3-030-72013-1_21

DO - 10.1007/978-3-030-72013-1_21

M3 - Chapter

SN - 978-3-030-72012-4

T3 - Lecture Notes in Computer Science

SP - 373

EP - 380

BT - Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part I

A2 - Groote, Jan Friso

A2 - Guldstrand Larsen, Kim

PB - Springer

T2 - 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021

Y2 - 27 March 2021 through 1 April 2021

ER -

Budde CE, Hartmanns A. Replicating RESTART with Prolonged Retrials: An Experimental Report. In Groote JF, Guldstrand Larsen K, editors, Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part I. Springer. 2021. p. 373-380. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-030-72013-1_21

Replicating RESTART with Prolonged Retrials: An Experimental Report

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this