CSiSAT: A Satisfiability Solver for SMT Formulas with Continuous Probability Distributions

Stochastic Satisfiability Modulo Theory (SSMT) [1] is a quantitative extension of classical Satisfiability Modulo Theory (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] and its continuous extension has been considered in our previous paper [3]. In this paper, we will discuss some issues regarding to its prototype implementation CSiSAT and test on some cases. The optimization strategies have been discussed which aim at enhancing the efficiency of CSiSAT. At last, a classical realtime scheduling problem is analyzed by using CSiSAT, where randomized execution time is considered.