h1

h2

h3

h4

h5
h6

001     755408
005     20230408005852.0
024 7 _ |2 HBZ
|a HT019983383
024 7 _ |2 Laufende Nummer
|a 37972
024 7 _ |2 datacite_doi
|a 10.18154/RWTH-2019-01829
037 _ _ |a RWTH-2019-01829
041 _ _ |a English
082 _ _ |a 004
100 1 _ |0 P:(DE-82)IDM01411
|a Kaminski, Benjamin Lucien
|b 0
|u rwth
245 _ _ |a Advanced weakest precondition calculi for probabilistic programs
|c vorgelegt von Benjamin Lucien Kaminski, M.SC.
|h online
246 _ 3 |a Erweiterte wp-Kalküle für Probabilistische Programme
|y German
260 _ _ |a Aachen
|c 2019
300 _ _ |a 1 Online-Ressource (xiv, 363 Seiten) : Illustrationen, Diagramme
336 7 _ |0 2
|2 EndNote
|a Thesis
336 7 _ |0 PUB:(DE-HGF)11
|2 PUB:(DE-HGF)
|a Dissertation / PhD Thesis
|b phd
|m phd
336 7 _ |2 BibTeX
|a PHDTHESIS
336 7 _ |2 DRIVER
|a doctoralThesis
336 7 _ |2 DataCite
|a Output Types/Dissertation
336 7 _ |2 ORCID
|a DISSERTATION
500 _ _ |a Veröffentlicht auf dem Publikationsserver der RWTH Aachen University
502 _ _ |a Dissertation, RWTH Aachen University, 2019
|b Dissertation
|c RWTH Aachen University
|d 2019
|g Fak01
|o 2019-02-08
520 3 _ |a Wir 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.
|l ger
520 _ _ |a We 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.
|l eng
536 _ _ |0 G:(EU-Grant)787914
|a FRAPPANT - Formal Reasoning About Probabilistic Programs: Breaking New Ground for Automation (787914)
|c 787914
|f ERC-2017-ADG
|x 0
588 _ _ |a Dataset connected to Lobid/HBZ
591 _ _ |a Germany
653 _ 7 |a Hoare logic
653 _ 7 |a almost-sure termination
653 _ 7 |a arithmetical hierarchy
653 _ 7 |a expected value
653 _ 7 |a formal methods
653 _ 7 |a induction
653 _ 7 |a invariant
653 _ 7 |a positive almost-sure termination
653 _ 7 |a probabilistic programming
653 _ 7 |a probabilistic programs
653 _ 7 |a probabilistic termination
653 _ 7 |a randomized algorithms
653 _ 7 |a variant
653 _ 7 |a verification
653 _ 7 |a weakest precondition
653 _ 7 |a weakest preexpectation
700 1 _ |0 P:(DE-82)IDM00048
|a Katoen, Joost-Pieter
|b 1
|e Thesis advisor
|u rwth
700 1 _ |0 P:(DE-82)109619
|a McIver, Annabelle
|b 2
|e Thesis advisor
856 4 _ |u https://publications.rwth-aachen.de/record/755408/files/755408.pdf
|y OpenAccess
856 4 _ |u https://publications.rwth-aachen.de/record/755408/files/755408_source.zip
|y Restricted
856 4 _ |u https://publications.rwth-aachen.de/record/755408/files/755408.gif?subformat=icon
|x icon
|y OpenAccess
856 4 _ |u https://publications.rwth-aachen.de/record/755408/files/755408.jpg?subformat=icon-1440
|x icon-1440
|y OpenAccess
856 4 _ |u https://publications.rwth-aachen.de/record/755408/files/755408.jpg?subformat=icon-180
|x icon-180
|y OpenAccess
856 4 _ |u https://publications.rwth-aachen.de/record/755408/files/755408.jpg?subformat=icon-640
|x icon-640
|y OpenAccess
856 4 _ |u https://publications.rwth-aachen.de/record/755408/files/755408.jpg?subformat=icon-700
|x icon-700
|y OpenAccess
909 C O |o oai:publications.rwth-aachen.de:755408
|p dnbdelivery
|p ec_fundedresources
|p VDB
|p driver
|p open_access
|p openaire
910 1 _ |0 I:(DE-588b)36225-6
|6 P:(DE-82)IDM01411
|a RWTH Aachen
|b 0
|k RWTH
910 1 _ |0 I:(DE-588b)36225-6
|6 P:(DE-82)IDM00048
|a RWTH Aachen
|b 1
|k RWTH
914 1 _ |y 2019
915 _ _ |0 StatID:(DE-HGF)0510
|2 StatID
|a OpenAccess
920 1 _ |0 I:(DE-82)121310_20140620
|k 121310
|l Lehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation)
|x 0
920 1 _ |0 I:(DE-82)080060_20170720
|k 080060
|l Graduiertenkolleg UnRAVeL
|x 1
920 1 _ |0 I:(DE-82)120000_20140620
|k 120000
|l Fachgruppe Informatik
|x 2
980 1 _ |a FullTexts
980 _ _ |a I:(DE-82)120000_20140620
980 _ _ |a I:(DE-82)080060_20170720
980 _ _ |a I:(DE-82)121310_20140620
980 _ _ |a UNRESTRICTED
980 _ _ |a VDB
980 _ _ |a phd

LibraryCollectionCLSMajorCLSMinorLanguageAuthor
Marc 21