Model Checking of Stochastic Hybrid Systems

Details
Category: Research
Last Updated on Monday, 26 November 2012 16:37

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.