@inproceedings{Ell2012,
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.}
}
@COMMENT{Bibtex file generated on }