The formal verification of probabilistic and hybrid (i.e., discrete-continuous) systems, each in isolation, is well-established and supported by efficient algorithms. Software tools like SpaceEx and Flow* support the reachability analysis of certain classes of hybrid systems, i.e., they can decide whether a given set of target states is reachable or not. Similarly, probabilistic model checkers like PRISM and MRMC rely on computing the probability to reach a set of states. Combining randomised and hybrid behavior leads to powerful models that pose formidable challenges for verification techniques. Reachability analysis for probabilistic hybrid systems has been addressed for simple model classes like probabilistic rectangular automata. Approaches for more expressive model classes such as discrete-time stochastic hybrid systems and stochastic hybrid automata all rely on abstraction. These abstractions are either time discretisations (such as gridding) or state-based abstractions. As a result, standard probabilistic model checkers or hybrid model checkers are employed. The main drawbacks of the existing approaches are:

• they often come without any guarantee of correctness—it is hard to bound the errors made by state-based abstraction
• they do not exploit verification techniques that combine hybrid and probabilistic behavior, and
• provide no useful diagnostic feedback in case a reachability property is refuted.

This dissertation project aims to develop novel approaches and powerful software tools for verifying probabilistic hybrid systems by adapting, extending and combining successful methods for probabilistic systems on the one hand and for hybrid systems on the other hand. Hybrid models, possibly with non-linear dynamics, with discrete probabilistic branching as well as restricted hybrid models with stochastic timing (such as piecewise continuous Markov processes, a simplified hybrid version of time-inhomogeneous continuous-time Markov chains (CTMCs)) will be considered. The focus will be on reachability analysis as well as bounded reachability. It will be investigated whether the flow-pipe technique underlying Flow* can be extended with randomisation. Furthermore, the plan is to combine techniques for counterexample generation for hybrid systems with those of probabilistic systems. Apart from the theoretical considerations, prototypical software tool-support will be developed and empirical evaluation will be carried out on different benchmark sets.