Constraint-Based Analysis of Probabilistic Hybrid Systems

Aiming at fully symbolic methods for the analysis of probabilistic hybrid systems, we recently introduced the notion of stochastic satisfiability modulo theories (SSMT) problems and the corresponding SiSAT solving algorithm. The notion of SSMT extends SMT with randomized (aka. stochastic) as well as existential and universal quantification as known from stochastic propositional satisfiability. In this paper, we describe the symbolic encoding of scheduled-event probabilistic hybrid automata by means of a case study from the networked automation system domain. We furthermore report on the SSMT solver SiSAT including recent enhancements in terms of solver performance, expressiveness of the input language, and handling of numerical issues. The significance of the performance enhancements is demonstrated by empirical results.