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.
This work was partially funded by NWO, NS, and ProRail project 15474 (SEQUOIA) and EU project 102112 (SUCCESS).
Chapter PDF
Similar content being viewed by others
References
Barbot, B., Haddad, S., Picaronny, C.: Coupling and importance sampling for statistical model checking. In: TACAS. LNCS, vol. 7214, pp. 331–346. Springer, Berlin Heidelberg (2012). https://doi.org/10.1007/978-3-642-28756-5_23
Budde, C.E.: Automation of Importance Splitting Techniques for Rare Event Simulation. Ph.D. thesis, FAMAF, Universidad Nacional de Córdoba, Córdoba, Argentina (2017), https://famaf.biblio.unc.edu.ar/cgi-bin/koha/opac-detail.pl?biblionumber=18143
Budde, C.E.: FIG: the Finite Improbability Generator. 4TU.Centre for Research Data (2020). https://doi.org/10.4121/uuid:1d5ddcd6-b3a9-4425-92b3-c46db98b7d8e
Budde, C.E., D’Argenio, P.R., Hartmanns, A.: Better automated importance splitting for transient rare events. In: SETTA. LNCS, vol. 10606, pp. 42–58. Springer (2017). https://doi.org/10.1007/978-3-319-69483-2_3
Budde, C.E., D’Argenio, P.R., Hartmanns, A., Sedwards, S.: A statistical model checker for nondeterminism and rare events. In: TACAS. LNCS, vol. 10806, pp. 340–358. Springer (2018). https://doi.org/10.1007/978-3-319-89963-3_20
Budde, C.E., D’Argenio, P.R., Monti, R.E.: Compositional construction of importance functions in fully automated importance splitting. In: VALUETOOLS. ICST (2016). https://doi.org/10.4108/eai.25-10-2016.2266501
Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: Quantitative model and tool interaction. In: TACAS. LNCS, vol. 10206, pp. 151–168. Springer (2017). https://doi.org/10.1007/978-3-662-54580-5_9
Cérou, F., Del Moral, P., Furon, T., Guyader, A.: Sequential Monte Carlo for rare event estimation. Statistics and Computing 22(3), 795–808 (2012). https://doi.org/10.1007/s11222-011-9231-6
Conway, R.: Some tactical problems in digital simulation. Management Science 10(1), 47–61 (1963). https://doi.org/10.1287/mnsc.10.1.47
D’Argenio, Pedro, Legay, Axel, Sedwards, Sean, Traonouez, Louis-Marie: Smart sampling for lightweight verification of Markov decision processes. International Journal on Software Tools for Technology Transfer 17(4), 469–484 (2015). https://doi.org/10.1007/s10009-015-0383-0
D’Argenio, P.R., Monti, R.E.: Input/Output Stochastic Automata with Urgency: Confluence and weak determinism. In: ICTAC. LNCS, vol. 11187, pp. 132–152. Springer (2018). https://doi.org/10.1007/978-3-030-02508-3_8
Dean, T., Dupuis, P.: Splitting for rare event simulation: A large deviation approach to design and analysis. Stochastic Processes and their Applications 119(2), 562–587 (2009). https://doi.org/10.1016/j.spa.2008.02.017
Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A Storm is coming: A modern probabilistic model checker. In: CAV. LNCS, vol. 10427, pp. 592–600. Springer (2017). https://doi.org/10.1007/978-3-319-63390-9_31
Garvels, M.J.J., van Ommeren, J.C.W., Kroese, D.P.: On the importance function in splitting simulation. Eur. Trans. Telecommun. 13(4), 363–371 (2002). https://doi.org/10.1002/ett.4460130408
Garvels, M.J.J.: The splitting method in rare event simulation. Ph.D. thesis, Department of Computer Science, University of Twente, Enschede, The Netherlands (2000), http://eprints.eemcs.utwente.nl/14291/.
Hartmanns, A., Hermanns, H.: The Modest Toolset: An integrated environment for quantitative modelling and verification. In: TACAS. LNCS, vol. 8413, pp. 593–598. Springer (2014). https://doi.org/10.1007/978-3-642-54862-8_51
Iglewicz, B., Hoaglin, D.: How to Detect and Handle Outliers. ASQC basic references in quality control, ASQC Quality Press (1993).
Jégourel, C., Legay, A., Sedwards, S.: Command-based importance sampling for statistical model checking. Theor. Comput. Sci. 649, 1–24 (2016). https://doi.org/10.1016/j.tcs.2016.08.009
Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: CAV. LNCS, vol. 6806, pp. 585–591. Springer (2011). https://doi.org/10.1007/978-3-642-22110-1_47
L’Ecuyer, P., Le Gland, F., Lezaud, P., Tuffin, B.: Splitting techniques. In: Rubino and Tuffin [25], pp. 39–61. https://doi.org/10.1002/9780470745403.ch3
Legay, A., Sedwards, S., Traonouez, L.M.: Plasma Lab: A modular statistical model checking platform. In: ISoLA. LNCS, vol. 9952, pp. 77–93 (2016). https://doi.org/10.1007/978-3-319-47166-2_6
Mediouni, B.L., Nouri, A., Bozga, M., Dellabani, M., Legay, A., Bensalem, S.: \(\cal{S}\)BIP 2.0: Statistical model checking stochastic real-time systems. In: ATVA. LNCS, vol. 11138, pp. 536–542. Springer (2018). https://doi.org/10.1007/978-3-030-01090-4_33
Monti, R.E.: Stochastic Automata for Fault Tolerant Concurrent Systems. Ph.D. thesis, FAMAF, Universidad Nacional de Córdoba, Córdoba, Argentina (2018).
Rubino, G., Tuffin, B.: Introduction to rare event simulation. In: Rubino and Tuffin [25], pp. 1–13. https://doi.org/10.1002/9780470745403.ch1
Rubino, G., Tuffin, B. (eds.): Rare Event Simulation Using Monte Carlo Methods. Wiley (2009). https://doi.org/10.1002/9780470745403
Ruijters, E., Reijsbergen, D., de Boer, P.T., Stoelinga, M.: Rare event simulation for dynamic fault trees. Reliability Engineering & System Safety 186, 220–231 (2019). https://doi.org/10.1016/j.ress.2019.02.004
Turati, P., Pedroni, N., Zio, E.: Advanced RESTART method for the estimation of the probability of failure of highly reliable hybrid dynamic systems. Reliability Engineering & System Safety 154(C), 117–126 (2016). https://doi.org/10.1016/j.ress.2016.04.020
Villén-Altamirano, J.: Importance functions for restart simulation of general Jackson networks. European Journal of Operational Research 203(1), 156–165 (2010). https://doi.org/10.1016/j.ejor.2009.07.013
Villén-Altamirano, J.: RESTART vs Splitting: A comparative study. Performance Evaluation 121–122, 38–47 (2018). https://doi.org/10.1016/j.peva.2018.02.002
Villén-Altamirano, J., Villén-Altamirano, M.: Rare event simulation of non-Markovian queueing networks using RESTART method. Simulation Modelling Practice and Theory 37, 70–78 (2013). https://doi.org/10.1016/j.simpat.2013.05.012
Villén-Altamirano, M., Villén-Altamirano, J.: RESTART: a method for accelerating rare event simulations. In: Queueing, Performance and Control in ATM (ITC-13). pp. 71–76. Elsevier (1991).
Wilson, E.B.: Probable inference, the law of succession, and statistical inference. Journal of the American Statistical Association 22(158), 209–212 (1927). https://doi.org/10.1080/01621459.1927.10502953
Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: CAV. LNCS, vol. 2404, pp. 223–235. Springer (2002). https://doi.org/10.1007/3-540-45657-0_17
Acknowledgments
The author thanks Arnd Hartmanns for excellent discussions that originally motivated and subsequently helped to shape this work.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Budde, C.E. (2020). FIG: The Finite Improbability Generator. In: Biere, A., Parker, D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science(), vol 12078. Springer, Cham. https://doi.org/10.1007/978-3-030-45190-5_27
Download citation
DOI: https://doi.org/10.1007/978-3-030-45190-5_27
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45189-9
Online ISBN: 978-3-030-45190-5
eBook Packages: Computer ScienceComputer Science (R0)