---
res:
bibo_abstract:
- This dissertation concerns the automatic verification of probabilistic systems
and programs with arrays by statistical and logical methods. Although statistical
and logical methods are different in nature, we show that they can be successfully
combined for system analysis. In the first part of the dissertation we present
a new statistical algorithm for the verification of probabilistic systems with
respect to unbounded properties, including linear temporal logic. Our algorithm
often performs faster than the previous approaches, and at the same time requires
less information about the system. In addition, our method can be generalized
to unbounded quantitative properties such as mean-payoff bounds. In the second
part, we introduce two techniques for comparing probabilistic systems. Probabilistic
systems are typically compared using the notion of equivalence, which requires
the systems to have the equal probability of all behaviors. However, this notion
is often too strict, since probabilities are typically only empirically estimated,
and any imprecision may break the relation between processes. On the one hand,
we propose to replace the Boolean notion of equivalence by a quantitative distance
of similarity. For this purpose, we introduce a statistical framework for estimating
distances between Markov chains based on their simulation runs, and we investigate
which distances can be approximated in our framework. On the other hand, we propose
to compare systems with respect to a new qualitative logic, which expresses that
behaviors occur with probability one or a positive probability. This qualitative
analysis is robust with respect to modeling errors and applicable to many domains.
In the last part, we present a new quantifier-free logic for integer arrays, which
allows us to express counting. Counting properties are prevalent in array-manipulating
programs, however they cannot be expressed in the quantified fragments of the
theory of arrays. We present a decision procedure for our logic, and provide several
complexity results.@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Przemyslaw
foaf_name: Daca, Przemyslaw
foaf_surname: Daca
foaf_workInfoHomepage: http://www.librecat.org/personId=49351290-F248-11E8-B48F-1D18A9856A87
bibo_doi: 10.15479/AT:ISTA:TH_730
dct_date: 2017^xs_gYear
dct_language: eng
dct_publisher: IST Austria@
dct_title: Statistical and logical methods for property checking@
...