Model Checking of Stochastic Hybrid Systems

Transition locality can also be used to design efficient disk based bounded model checking algorithms for discrete time stochastic processes (namely Markov Chains) [STTT 2006, FMCAD 2004, CHARME 2003, ICTCS 2003]. The resulting tool allows verification (and thus reliability assessment) of systems out of reach for other model checkers.