Verification of Stochastic Systems by Stochastic Satisfiability Modulo Theories with Continuous Domain (CSSMT)

Yang Gao
Stochastic Satisfiability Modulo Theories (SSMT) is a quantitative extension of Satisfiability Modulo Theories (SMT) inspired by stochastic logics. It extends SMT by randomized quantifiers, facilitating capture of stochastic game properties in the logic, like reachability analysis of hybrid-state Markov decision processes. Solving SSMT formulae with quantification over finite and thus discrete domain has been addressed by Tino Teige et al. A major limitation of the SSMT solving approach is that all quantifiers are confined to range over finite domains. As this implies that the support of probability distributions have to be finite, a large number of phenomena cannot be expressed within the SSMT framework. To overcome this limitation, this thesis relaxes the constraints on the domains of randomized variables, now also admitting dense probability distributions in SSMT solving, which yields SSMT over continuous quantifier domains (CSSMT).
Novemeber / 2017