FIG: The Finite Improbability Generator

Carlos E. Budde

doi:10.1007/978-3-030-45190-5_27

FIG: The Finite Improbability Generator

Carlos E. Budde^*

^*Corresponding author for this work

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

4 Citations (Scopus)

77 Downloads (Pure)

Abstract

This paper introduces the statistical model checker FIGV, that estimates transient and steady-state reachability properties in stochastic automata. This software tool specialises in Rare Event Simulation via importance splitting, and implements the algorithms RESTART and Fixed Effort. FIG is push-button automatic since the user need not define an importance function: this function is derived from the model specification plus the property query. The tool operates with Input/Output Stochastic Automata with Urgency, aka IOSA models, described either in the native syntax or in the JANI exchange format. The theory backing FIG has demonstrated good efficiency, comparable to optimal importance splitting implemented ad hoc for specific models. Written in C++, FIG can outperform other state-of-the-art tools for Rare Event Simulation.

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	Armin Biere, David Parker
Publisher	Springer
Pages	483-491
Number of pages	9
ISBN (Electronic)	978-3-030-45190-5
ISBN (Print)	9783030451899
DOIs	https://doi.org/10.1007/978-3-030-45190-5_27
Publication status	Published - 17 Apr 2020
Event	26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020 - Dublin, Ireland Duration: 25 Apr 2020 → 30 Apr 2020 Conference number: 26

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12078 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020
Abbreviated title	TACAS
Country/Territory	Ireland
City	Dublin
Period	25/04/20 → 30/04/20

Access to Document

10.1007/978-3-030-45190-5_27Licence: CC BY

10.1007_978-3-030-45190-5_27Final published version, 330 KBLicence: CC BY

Cite this

Budde, C. E. (2020). FIG: The Finite Improbability Generator. In A. Biere, & D. Parker (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. 483-491). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12078 LNCS). Springer. https://doi.org/10.1007/978-3-030-45190-5_27

Budde, Carlos E. / FIG: The Finite Improbability Generator. 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 / Armin Biere ; David Parker. Springer, 2020. pp. 483-491 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{d13c5cae40d14635bf940d9c332768c1,

title = "FIG: The Finite Improbability Generator",

abstract = "This paper introduces the statistical model checker FIGV, that estimates transient and steady-state reachability properties in stochastic automata. This software tool specialises in Rare Event Simulation via importance splitting, and implements the algorithms RESTART and Fixed Effort. FIG is push-button automatic since the user need not define an importance function: this function is derived from the model specification plus the property query. The tool operates with Input/Output Stochastic Automata with Urgency, aka IOSA models, described either in the native syntax or in the JANI exchange format. The theory backing FIG has demonstrated good efficiency, comparable to optimal importance splitting implemented ad hoc for specific models. Written in C++, FIG can outperform other state-of-the-art tools for Rare Event Simulation.",

author = "Budde, {Carlos E.}",

year = "2020",

month = apr,

day = "17",

doi = "10.1007/978-3-030-45190-5_27",

language = "English",

isbn = "9783030451899",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "483--491",

editor = "Armin Biere and David Parker",

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 = "Germany",

note = "26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, TACAS ; Conference date: 25-04-2020 Through 30-04-2020",

}

Budde, CE 2020, FIG: The Finite Improbability Generator. in A Biere & D Parker (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 (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12078 LNCS, Springer, pp. 483-491, 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, Dublin, Ireland, 25/04/20. https://doi.org/10.1007/978-3-030-45190-5_27

FIG: The Finite Improbability Generator. / Budde, Carlos E.
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. / Armin Biere; David Parker. Springer, 2020. p. 483-491 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12078 LNCS).

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

TY - CHAP

T1 - FIG: The Finite Improbability Generator

AU - Budde, Carlos E.

N1 - Conference code: 26

PY - 2020/4/17

Y1 - 2020/4/17

N2 - This paper introduces the statistical model checker FIGV, that estimates transient and steady-state reachability properties in stochastic automata. This software tool specialises in Rare Event Simulation via importance splitting, and implements the algorithms RESTART and Fixed Effort. FIG is push-button automatic since the user need not define an importance function: this function is derived from the model specification plus the property query. The tool operates with Input/Output Stochastic Automata with Urgency, aka IOSA models, described either in the native syntax or in the JANI exchange format. The theory backing FIG has demonstrated good efficiency, comparable to optimal importance splitting implemented ad hoc for specific models. Written in C++, FIG can outperform other state-of-the-art tools for Rare Event Simulation.

AB - This paper introduces the statistical model checker FIGV, that estimates transient and steady-state reachability properties in stochastic automata. This software tool specialises in Rare Event Simulation via importance splitting, and implements the algorithms RESTART and Fixed Effort. FIG is push-button automatic since the user need not define an importance function: this function is derived from the model specification plus the property query. The tool operates with Input/Output Stochastic Automata with Urgency, aka IOSA models, described either in the native syntax or in the JANI exchange format. The theory backing FIG has demonstrated good efficiency, comparable to optimal importance splitting implemented ad hoc for specific models. Written in C++, FIG can outperform other state-of-the-art tools for Rare Event Simulation.

UR - http://www.scopus.com/inward/record.url?scp=85084003331&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-45190-5_27

DO - 10.1007/978-3-030-45190-5_27

M3 - Chapter

AN - SCOPUS:85084003331

SN - 9783030451899

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 483

EP - 491

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 - Biere, Armin

A2 - Parker, David

PB - Springer

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

Y2 - 25 April 2020 through 30 April 2020

ER -

Budde CE. FIG: The Finite Improbability Generator. In Biere A, Parker D, 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. 2020. p. 483-491. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-45190-5_27

FIG: The Finite Improbability Generator

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Software artefact for FIG: the Finite Improbability Generator

Cite this

FIG: The Finite Improbability Generator

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Datasets

Software artefact for FIG: the Finite Improbability Generator

Cite this