<div class="csl-bib-body">
<div class="csl-entry">Stankovic, M. (2023). <i>Moment-based loop analysis</i> [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2023.113863</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2023.113863
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/187383
-
dc.description
Zusammenfassung in deutscher Sprache
-
dc.description.abstract
In this thesis, we explore automated analysis of loops of probabilistic programs (PPs). We look specifically at finding a quantitative loop invariant: a property of a given loop that describes its behaviour. Loop invariants are key for reasoning about program loops. In the context of probabilistic programs, variables represent distributions, and the invariant needs to capture the statistical properties of these distributions. In our work, we focus on computing so-called moment-based invariants (MBIs), invariant properties that describe the expected value and higher (and mixed) moments of program variables. While it is not feasible to compute all moments, which would fully characterize the underlying distribution, our methods are able to compute moments of arbitrary order, hence allowing us to capture the loop properties relatively precisely. As one of the main results in this thesis, we give a characterization of Prob-solvable loops, a class of PP loops, for which MBIs can be, in principle, always computed. We also describe a fully automated method of computing MBIs of arbitrary order for any program of this class. The method is implemented and evaluated on several challenging benchmarks from the literature. In the second part of the thesis, we study how moment-based analysis of Prob-solvable loops and MBIs can be applied to reasoning about various challenges in Bayesian networks (BNs). We extend the framework introduced earlier to accommodate encoding BNs as PPs and also provide a way to encode several tasks in BN analysis as computing MBIs in a corresponding PP - such as exact inference, expected number of samples, or sensitivity analysis. In the last part of the thesis, we briefly discuss extensions of this work. We fully characterize the class of programs for which MBIs can be computed (moment-computable programs) and investigate how to automatically estimate probability distributions from MBIs. We also consider programs that are not moment-computable, for which we look at combinations of variables and approximations.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
Probabilistic Programs
en
dc.subject
Higher Moments
en
dc.subject
Linear Recurrences
en
dc.subject
Distribution Recovery
en
dc.subject
Non-linear Updates
en
dc.subject
Invariant Synthesis
en
dc.subject
Bayesian Networks
en
dc.subject
Static Analysis
en
dc.title
Moment-based loop analysis
en
dc.type
Thesis
en
dc.type
Hochschulschrift
de
dc.rights.license
In Copyright
en
dc.rights.license
Urheberrechtsschutz
de
dc.identifier.doi
10.34726/hss.2023.113863
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Miroslav Stankovic
-
dc.publisher.place
Wien
-
tuw.version
vor
-
tuw.thesisinformation
Technische Universität Wien
-
dc.contributor.assistant
Bartocci, Ezio
-
tuw.publication.orgunit
E192 - Institut für Logic and Computation
-
dc.type.qualificationlevel
Doctoral
-
dc.identifier.libraryid
AC16893455
-
dc.description.numberOfPages
88
-
dc.thesistype
Dissertation
de
dc.thesistype
Dissertation
en
tuw.author.orcid
0000-0001-5978-7475
-
dc.rights.identifier
In Copyright
en
dc.rights.identifier
Urheberrechtsschutz
de
tuw.advisor.staffStatus
staff
-
tuw.assistant.staffStatus
staff
-
tuw.advisor.orcid
0000-0002-8299-2714
-
tuw.assistant.orcid
0000-0002-8004-6601
-
item.fulltext
with Fulltext
-
item.grantfulltext
open
-
item.languageiso639-1
en
-
item.mimetype
application/pdf
-
item.openairetype
doctoral thesis
-
item.cerifentitytype
Publications
-
item.openaccessfulltext
Open Access
-
item.openairecristype
http://purl.org/coar/resource_type/c_db06
-
crisitem.author.dept
E191-01 - Forschungsbereich Cyber-Physical Systems