Bounded model checking of probabilistic hybrid automata

By Tino Teige

In this lecture we will present a technology for the symbolic analysis of probabilistic bounded reachability problems of PHAs. This fully symbolic treatment of the hybrid discrete-continuous state space as well as of the system's transition relation including probabilistic events is facilitated by a predicative encoding of the PHA. Akin to the non-probabilistic case, the next-state relation is mapped to a logical formula involving rich arithmetic constraints, giving rise to a satisfiability modulo theories (SMT) problem. To describe probabilistic choices in system executions, we will use randomized quantifiers as known from stochastic propositional satisfiability (SSAT) problems. Together with existential and universal quantification, this results in the concept of stochastic satisfiability modulo theories (SSMT). The classical quantifiers are used to resolve the non-determinism in the system by the desired, worst-case or best-case, policy.

Based on this encoding, a symbolic approach to the reachability analysis of PHA is probabilistic bounded model checking (PBMC). Given a temporal specification to be checked, the idea of PBMC is to unroll the next-state relation of the PHA to some given finite depth k and to augment it with a corresponding finite unravelling of the tableau of the temporal formula. The resulting SSMT problem is then satisfiable with probability p iff the PHA fulfills the specification with probability p along all its traces of depth up to k. For quantitative safety requirements like "The probability of a fatal system error must be always below 0.5%!", this reduction to SSMT enables a falsification procedure by successively solving PBMC formulas for increasing

depths k.

Completing the symbolic analysis framework, we will present an algorithm to compute the satisfaction probabilities of SSMT problems. This SSMT algorithm builds on an SMT algorithm to check satisfiability of quantifier-free subproblems. To further cope with randomized, existential, and universal quantifiers present in SSMT, an additional layer is added that traverses the Cartesian product of the domains of the quantified variables and computes the satisfaction probabilities for the individual quantifiers. However, that naive

approach is far from scalable as it has to solve one SMT subproblem per element of the Cartesian product of the quantifier ranges, that is exponential in the number of quantified variables. To overcome that scalability issue, we will present some aggressive pruning rules that save visits to major parts of the quantifier ranges, and are instrumental to the efficiency of the SSMT tool.