November 27th：

Title：Perturbation Analysis in Verification of Discrete-Time Markov Chains

Lecturer：Professor Yuan Feng（University of Technology Sydney）

Time：10：00 - 11：00, November 27(Friday),2015

Location: Room 1002, Science Building  B

Abstract：

        Probabilistic model checking is a verification technique that has been the focus of intensive research for over a decade. One important issue with probabilistic model checking, which is crucial for its practical significance but is overlooked by the state-of-the-art largely, is the potential discrepancy between a stochastic model and the real-world system it represents when the model is built from statistical data. In the worst case, a tiny but nontrivial change to some model quantities might lead to is leading or even invalid verification results.

       To address this issue, we present a mathematical characterisation of the consequence of model perturbations on the verification results. The formal model is a parametric variant of discrete-time Markov chains equipped with a vector norm to measure the perturbation. Our main contributions include orithms and tight complexity bounds for calculating both non-asymptotic bounds and asymptotic bounds with respect to three perturbation distances.

       This talk is based on a paper presented at Concur’14 and another one conditionally accepted by IEEE Transactions on Software Engineering.

Biography：

        Professor Yuan Feng is a core member of the Centre for Quantum Computation and Intelligent Systems (QCIS) at UTS. He received his BS degree in Applied Mathematics and PhD dgree in Computer Science from Tsinghua University in 1999 and 2004, respectively. Before joining UTS in 2009, he was an Associate Professor at the Department of Computer Science and Technology, Tsinghua University. Prof. Yuan Feng’s research interests include the theory of quantum information and quantum computation, quantum programming, and probabilistic systems.