PhD Comprehensive Seminar | Zhibing Sun, Verification of Stochastic Systems

Candidate

Zhibing Sun | Applied Mathematics, University of Waterloo

Title

Verification of Stochastic Systems

Abstract

We consider the verification of ω-regular properties of the discrete-time continuous-state stochastic systems. We adopt the abstraction-based method and use Interval-valued Markov chains(IMC) as our abstraction. We first introduce the verification of a reachability problem followed by the verification of ω-regular properties of Markov chains. Then we show why things are getting much more complicated as we apply such methods to the verification problems of IMCs and what we can solve.