Perturbation Analysis in Verification of Discrete-Time Markov Chains

报告题目：Perturbation Analysis in Verification of Discrete-Time Markov Chains

报告人：Yuan Feng教授（University of Technology Sydney）

主持人：邓玉欣 教授

时间：2015-11-27 周五 10：00-11：00

地点：中北校区理科大楼1002室

报告摘要：

    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 isleading 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.

报告人简介：

    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 gree 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.