A solving procedure for stochastic satisfiability modulo theories with continuous domain

Abstract

Stochastic Satisfiability Modulo Theories (SSMT) [1] is a quantitative extension of classical Satisfiability Modulo Theories (SMT) inspired by stochastic logics. It extends SMT by the usual as well as randomized quantifiers, facilitating capture of stochastic game properties in the logic, like reachability analysis of hybrid-state Markov decision processes. Solving for SSMT formulae with quantification over finite and thus discrete domain has been addressed by Tino Teige et al. [2]. In this paper, we extend their work to SSMT over continuous quantifier domains (CSSMT) in order to enable capture of continuous disturbances and uncertainty in hybrid systems. We extend the semantics of SSMT and introduce a corresponding solving procedure. A simple case study is pursued to demonstrate applicability of our framework to reachability problems in hybrid systems.