nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

The Probabilistic Termination Tool Amber

verfasst von : Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács

Erschienen in: Formal Methods

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We describe the Amber tool for proving and refuting the termination of a class of probabilistic while-programs with polynomial arithmetic, in a fully automated manner. Amber combines martingale theory with properties of asymptotic bounding functions and implements relaxed versions of existing probabilistic termination proof rules to prove/disprove (positive) almost sure termination of probabilistic loops. Amber supports programs parameterized by symbolic constants and drawing from common probability distributions. Our experimental comparisons give practical evidence of Amber outperforming existing state-of-the-art tools.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel HyperProb: A Model Checker for Probabilistic Hyperproperties

Nächstes Kapitel Model Checking Collision Avoidance of Nonlinear Autonomous Vehicles

https://github.com/probing-lab/amber.

https://github.com/lark-parser/lark.

https://github.com/diofant/diofant.

Agrawal, S., Chatterjee, K., Novotný, P.: Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. Proc. of POPL 2, 1–32 (2017). https://doi.org/10.1145/3158122CrossRef

Avanzini, M., Moser, G., Schaper, M.: A modular cost analysis for probabilistic programs. Proc. of OOPSLA 4, 1–30 (2020). https://doi.org/10.1145/3428240CrossRef

Bartocci, E., Kovács, L., Stankovič, M.: Analysis of bayesian networks via prob-solvable loops. In: Pun, V.K.I., Stolz, V., Simao, A. (eds.) ICTAC 2020. LNCS, vol. 12545, pp. 221–241. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-64276-1_12CrossRefMATH

Bartocci, E., Kovács, L., Stankovic, M.: Mora - automatic generation of moment-based invariants. In: Proceedings of TACAS (2020). https://doi.org/10.1007/978-3-030-45190-5

Bournez, O., Garnier, F.: Proving positive almost-sure termination. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 323–337. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-32033-3_24CrossRef

Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 511–526. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_34CrossRef

Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through positivstellensatz’s. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 3–22. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_1CrossRef

Chatterjee, K., Fu, H., Novotný, P.: Termination Analysis of Probabilistic Programs with Martingales. Foundations of Probabilistic Programming, pp. 221–258 (2020). https://doi.org/10.1017/9781108770750.008

Chatterjee, K., Novotný, P., Zikelic, D.: Stochastic invariants for probabilistic termination. In: Proceedings. of POPL (2017). https://doi.org/10.1145/3009837.3009873

10.

Chen, J., He, F.: Proving almost-sure termination by omega-regular decomposition. In: Proceedings of PLDI (2020). https://doi.org/10.1145/3385412.3386002

11.

Esparza, J., Gaiser, A., Kiefer, S.: Proving termination of probabilistic programs using patterns. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 123–138. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_14CrossRef

12.

Ferrer Fioriti, L.L.M., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: Proceedings of POPL (2015). https://doi.org/10.1145/2676726.2677001

13.

Ghahramani, Z.: Probabilistic machine learning and artificial intelligence. Nature 521, 452–459 (2015). https://doi.org/10.1038/nature14541CrossRef

14.

Huang, M., Fu, H., Chatterjee, K.: New approaches for almost-sure termination of probabilistic programs. In: Ryu, S. (ed.) APLAS 2018. LNCS, vol. 11275, pp. 181–201. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02768-1_11CrossRef

15.

Kaminski, B.L., Katoen, J.P.: On the hardness of almost–sure termination. In: Italiano, G.F., Pighizzini, G., Sannella, D.T. (eds.) MFCS 2015. LNCS, vol. 9234, pp. 307–318. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48057-1_24CrossRef

16.

McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.P.: A new proof rule for almost-sure termination. Proc. of ACM Program. Lang. (2018). https://doi.org/10.1145/3158121CrossRef

17.

Merkel, D.: Docker: lightweight linux containers for consistent development and deployment. Linux J. 239, 2 (2014)

18.

Meyer, F., Hark, M., Giesl, J.: Inferring expected runtimes of probabilistic integer programs using expected sizes. In: TACAS 2021. LNCS, vol. 12651, pp. 250–269. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-72016-2_14CrossRefMATH

19.

Moosbrugger, M., Bartocci, E., Katoen, J.P., Kovács, L.: Automated termination analysis of polynomial probabilistic programs. In: ESOP 2021. LNCS, vol. 12648, pp. 491–518. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-72019-3_18CrossRef

20.

Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: resource analysis for probabilistic programs. In: Proceedings of PLDI (2018). https://doi.org/10.1145/3192366.3192394

Titel: The Probabilistic Termination Tool Amber
verfasst von: Marcel Moosbrugger
Ezio Bartocci
Joost-Pieter Katoen
Laura Kovács
Verlag: Springer International Publishing
Buch: Formal Methods
Print ISBN: 978-3-030-90869-0

Electronic ISBN: 978-3-030-90870-6

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-90870-6_36

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner