PhD Comprehensive Exam | Zhibing Sun, Verification of Stochastic Systems

MS Teams (please email amgrad@uwaterloo.ca for the meeting link) 

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 $\omega$-regular properties of Markov chains. We give convergence analysis to the quantitative reachability problem. Then we give a detailed description of the behavior of interval-valued Markov chain.

We give a big picture of how to convert the verification of reachability problem from not solvable to solvable both theoretically and in practice. We first consider the optimization problems with memoryless adversaries, and then show that the history dependent ones would have no better performance. We show that the optimum solution exists, a local optimum is the global optimum, and the optimum solution of all the states can be achieved at the same time. We give algorithms for the qualitative maximum and minimum reachability problems. We give a detailed description and analysis of an algorithm for the quantitative maximum reachability problem. For the verification of ω-regular properties, we introduce the existing results and state the difficulties for the qualitative problem.