Model-Checking of stochastic systems based on approximation. (Work in progress)

Blaise Genest ( IRISA Lab, Rennes, France )

30 years of Model Checking taught us that automata based methods can be used in the verification of real life system, granted that powerful abstraction refinement techniques are used. Our aim is to propose such an abstraction refinement for stochastic systems and distribution-based properties. The basic idea is to approximate the precise probabilities. The refinement step (in term of more precise computation) will be triggered only if the error made is too big to conclude. An important tool for analyzing the error is the contracting factor of irreducible and aperiodic chains. This can be used to bound the error made while approximating the transient values generated by large Markov Chains represented as Dynamic Bayesian Networks. This can also be used to approximate the steady state behavior of (general) Markov Chain. In the former case, approximation is needed because of the complexity of the problem. In the latter case, model checking the exact behavior of general Markov Chains is as hard as the Skolem problem.