h1

000755408 001__ 755408
000755408 005__ 20230408005852.0
000755408 0247_ $$2HBZ$$aHT019983383
000755408 0247_ $$2Laufende Nummer$$a37972
000755408 0247_ $$2datacite_doi$$a10.18154/RWTH-2019-01829
000755408 037__ $$aRWTH-2019-01829
000755408 041__ $$aEnglish
000755408 082__ $$a004
000755408 1001_ $$0P:(DE-82)IDM01411$$aKaminski, Benjamin Lucien$$b0$$urwth
000755408 245__ $$aAdvanced weakest precondition calculi for probabilistic programs$$cvorgelegt von Benjamin Lucien Kaminski, M.SC.$$honline
000755408 246_3 $$aErweiterte wp-Kalküle für Probabilistische Programme$$yGerman
000755408 260__ $$aAachen$$c2019
000755408 300__ $$a1 Online-Ressource (xiv, 363 Seiten) : Illustrationen, Diagramme
000755408 3367_ $$02$$2EndNote$$aThesis
000755408 3367_ $$0PUB:(DE-HGF)11$$2PUB:(DE-HGF)$$aDissertation / PhD Thesis$$bphd$$mphd
000755408 3367_ $$2BibTeX$$aPHDTHESIS
000755408 3367_ $$2DRIVER$$adoctoralThesis
000755408 3367_ $$2DataCite$$aOutput Types/Dissertation
000755408 3367_ $$2ORCID$$aDISSERTATION
000755408 500__ $$aVeröffentlicht auf dem Publikationsserver der RWTH Aachen University
000755408 502__ $$aDissertation, RWTH Aachen University, 2019$$bDissertation$$cRWTH Aachen University$$d2019$$gFak01$$o2019-02-08
000755408 5203_ $$aWir studieren die quantitative Analyse probabilistischer Programme. Dabei untersuchen wir vornehmlich zwei Aspekte: Die Analysetechniken selbst, sowie die komplexitäts- bzw. berechenbarkeitstheoretische Schwere der entsprechenden Analyseprobleme. In Bezug auf die Analysetechniken geben wir zunächst eine umfassende Einführung in den Kalkül der Schwächsten Vorerwartungen à la McIver & Morgan - ein Kalkül für die Verifikation probabilistischer Programme, der auf Dijkstras Kalkül der Schwächsten Vorbedingungen für Programme mit Nichtdeterminismus und Kozens Probabilistischer Dynamischer Aussagenlogik für probabilistische Programme aufbaut. Anschließend entwickeln wir weitergehende Kalküle für probabilistische Programme im Stile McIver & Morgans, welche dazu geeignet sind, Analysen über - erwartete Laufzeiten, - bedingte Erwartungswerte und bedingte Wahrscheinlichkeiten, und - Erwartungswerte von Zufallsvariablen mit gemischtem Vorzeichen zu fahren. Wie auch Dijkstras Kalkül sind unsere Kalküle induktiv über die Programmstruktur definiert und erlauben somit eine modulare Analyse auf Quelltextebene. Ein besonderes Augenmerk legen wir auf Regeln, welche die Analyse von Schleifen ermöglichen. Der zweite Aspekt, den wir untersuchen, ist die inhärente berechenbarkeitstheoretische Schwere der Analyse probabilistischer Programme, welche unabhängig von der verwendeten Analysetechnik selbst ist. Im Speziellen untersuchen wir dazu die Schwere der Approximation von Erwartungswerten und Kovarianzen. Wir zeigen, dass untere Schranken für Erwartungswerte nicht berechenbar, aber rekursiv aufzählbar sind, obere Schranken jedoch nicht rekursiv aufzählbar sind. Für Kovarianzen zeigen wir, dass weder obere noch untere Schranken rekursiv aufzählbar sind. Desweiteren untersuchen wir die Schwere der Entscheidbarkeit der Terminierung probabilistischer Programme. Während wir dazu zwar unterschiedliche Auffassungen eines probabilistischen Terminierungsbegriffs untersuchen, beispielsweise fast-sichere Terminierung oder Terminierung innerhalb endlicher erwarteter Zeit (auch positive fast-sichere Terminierung genannt), zeigen wir, dass die Terminierung probabilistischer Programme im Allgemeinen echt schwerer zu entscheiden ist als die Terminierung nicht-probabilistischer Programme.$$lger
000755408 520__ $$aWe study quantitative reasoning about probabilistic programs. In doing so, we investigate two main aspects: The reasoning techniques themselves and the computational hardness of that reasoning. As for the former aspect, we first give a comprehensive introduction to weakest preexpectation reasoning à la McIver & Morgan - a reasoning technique for the verification of probabilistic programs that builds on Dijkstra's weakest precondition calculus for programs with nondeterminism and Kozen's probabilistic propositional dynamic logic for probabilistic programs. We then develop advanced weakest-preexpectation-style calculi for probabilistic programs that enable reasoning about - expected runtimes, - conditional expected values and conditional probabilities, and - expected values of mixed-sign random variables. As with Dijkstra's calculus, our calculi are defined inductively on the program structure and thus allow for compositional reasoning on source code level. We put a special emphasis on proof rules for reasoning about loops. The second aspect we study is the inherent computational hardness of reasoning about probabilistic programs, which is independent from the employed analysis technique. In particular, we study the hardness of approximating expected values and (co)variances. We show that lower bounds on expected values are not computable but computably enumerable, whereas upper bounds are not computably enumerable. For covariances, we show that neither lower nor upper bounds are computably enumerable. Furthermore, we study the hardness of deciding termination of probabilistic programs. While we study different notions of probabilistic termination, for instance almost-sure termination or termination within finite expected time (also known as positive almost-sure termination), we show that deciding termination of probabilistic programs is generally strictly harder than deciding termination of nonprobabilistic programs.$$leng
000755408 536__ $$0G:(EU-Grant)787914$$aFRAPPANT - Formal Reasoning About Probabilistic Programs: Breaking New Ground for Automation (787914)$$c787914$$fERC-2017-ADG$$x0
000755408 588__ $$aDataset connected to Lobid/HBZ
000755408 591__ $$aGermany
000755408 653_7 $$aHoare logic
000755408 653_7 $$aalmost-sure termination
000755408 653_7 $$aarithmetical hierarchy
000755408 653_7 $$aexpected value
000755408 653_7 $$aformal methods
000755408 653_7 $$ainduction
000755408 653_7 $$ainvariant
000755408 653_7 $$apositive almost-sure termination
000755408 653_7 $$aprobabilistic programming
000755408 653_7 $$aprobabilistic programs
000755408 653_7 $$aprobabilistic termination
000755408 653_7 $$arandomized algorithms
000755408 653_7 $$avariant
000755408 653_7 $$averification
000755408 653_7 $$aweakest precondition
000755408 653_7 $$aweakest preexpectation
000755408 7001_ $$0P:(DE-82)IDM00048$$aKatoen, Joost-Pieter$$b1$$eThesis advisor$$urwth
000755408 7001_ $$0P:(DE-82)109619$$aMcIver, Annabelle$$b2$$eThesis advisor
000755408 8564_ $$uhttps://publications.rwth-aachen.de/record/755408/files/755408.pdf$$yOpenAccess
000755408 8564_ $$uhttps://publications.rwth-aachen.de/record/755408/files/755408_source.zip$$yRestricted
000755408 8564_ $$uhttps://publications.rwth-aachen.de/record/755408/files/755408.gif?subformat=icon$$xicon$$yOpenAccess
000755408 8564_ $$uhttps://publications.rwth-aachen.de/record/755408/files/755408.jpg?subformat=icon-1440$$xicon-1440$$yOpenAccess
000755408 8564_ $$uhttps://publications.rwth-aachen.de/record/755408/files/755408.jpg?subformat=icon-180$$xicon-180$$yOpenAccess
000755408 8564_ $$uhttps://publications.rwth-aachen.de/record/755408/files/755408.jpg?subformat=icon-640$$xicon-640$$yOpenAccess
000755408 8564_ $$uhttps://publications.rwth-aachen.de/record/755408/files/755408.jpg?subformat=icon-700$$xicon-700$$yOpenAccess
000755408 909CO $$ooai:publications.rwth-aachen.de:755408$$popenaire$$popen_access$$pdriver$$pVDB$$pec_fundedresources$$pdnbdelivery
000755408 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM01411$$aRWTH Aachen$$b0$$kRWTH
000755408 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM00048$$aRWTH Aachen$$b1$$kRWTH
000755408 9141_ $$y2019
000755408 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess
000755408 9201_ $$0I:(DE-82)121310_20140620$$k121310$$lLehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation)$$x0
000755408 9201_ $$0I:(DE-82)080060_20170720$$k080060$$lGraduiertenkolleg UnRAVeL$$x1
000755408 9201_ $$0I:(DE-82)120000_20140620$$k120000$$lFachgruppe Informatik$$x2
000755408 961__ $$c2019-03-19T09:49:56.746914$$x2019-02-18T17:57:45.922468$$z2019-03-19T09:49:56.746914
000755408 9801_ $$aFullTexts
000755408 980__ $$aI:(DE-82)120000_20140620
000755408 980__ $$aI:(DE-82)080060_20170720
000755408 980__ $$aI:(DE-82)121310_20140620
000755408 980__ $$aUNRESTRICTED
000755408 980__ $$aVDB
000755408 980__ $$aphd