SAT-Modulo-Theory based Analysis of Probabilistic Hybrid Systems

The framework of hybrid discrete-continuous systems becomes increasingly popular for modeling and verifying large real-world, often safety-critical, embedded systems, e.g. in the car and aviation industry. In contrast to purely discrete models, like Kripke struc-tures, hybrid systems additionally show continuous behavior usually modeled by differen-tial equations. Therefore, the state space of a hybrid system is infinite and given by the Cartesian product of the system modes and the discrete and continuous system variable do-mains. The system can change its current mode by a potentially non-deterministic choice of a transition to another mode, while during residing in a mode the variables continu-ously evolve over time. This rich formalism allows a direct and expressive modelling of real-world systems. On the other hand, the complexity of model checking such a system against requirements grows with increasing expressiveness of the modeling framework. While the state reachability problem of very restricted subclasses (timed automata) is de-cidable, it becomes undecidable in general when adding some small extra functionality (e.g., stopwatch automata). Nevertheless, industrial needs motivate the development of ef-ficient model-checking algorithms for richer classes of hybrid systems involving arbitrar