@inproceedingsEll2012,
Author = {Ellen, Christian and Gerwinn, Sebastian and Fränzle, Martin},
Title = {Confidence Bounds for Statistical Model Checking of Probabilistic Hybrid Systems},
Year = {2012},
Pages = {123-138},
Month = {09},
Editor = {Springer},
Series = {LNCS},
Edition = {7595},
Isbn = {978-3-642-33364-4},
Booktitle = {Formal Modeling and Analysis of Timed Systems - 10th International Conference, FORMATS 2012, London, UK},
type = {inproceedings},
note = {Model checking of technical systems is a common and demanding
task. The behavior of such systems can often be characterized
using hybrid automata, leading to verification problems within the
first-order logic over the reals. The applicability of },
Abstract = {Model checking of technical systems is a common and demanding
task. The behavior of such systems can often be characterized
using hybrid automata, leading to verification problems within the
first-order logic over the reals. The applicability of logic-based
formalisms to a wider range of systems has recently been increased
by introducing quantifiers into satisfiability modulo theory (SMT)
approaches to solve such problems, especially randomized
quantifiers, resulting in stochastic satisfiability modulo theory
(SSMT). These quantifiers combine non-determinism and
stochasticity, thereby allowing to represent models such as Markov
decision processes. While algorithms for exact model checking in
this setting exist, their scalability is limited due to the
computational complexity which increases with the number of
quantified variables. Additionally, these methods become infeasible
if the domain of the quantified variables, randomized variables in
particular, becomes too large or even infinite. In this paper, we
present an approximation algorithm based on confidence intervals
obtained from sampling which allow for an explicit trade-off between
accuracy and computational effort. Although the algorithm gives only
approximate results in terms of confidence intervals, it is still
guaranteed to converge to the exact solution. To further increase
the performance of the algorithm, we adopt search strategies based
on the upper bound confidence algorithm UCB originally used to
solve a similar problem, the multi-armed bandit. Preliminary results
show that the proposed algorithm can improve the performance
in comparison to existing SSMT solvers, especially in the presence of
many randomized quantified variables.}
@COMMENTBibtex file generated on