文章基本信息

标题：Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes
本地全文：下载
作者：Sadegh Esmaeil Zadeh Soudjani ; Alessandro Abate ; Rupak Majumdar 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2015
卷号：42
页码：169-183
DOI：10.4230/LIPIcs.CONCUR.2015.169
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：We study the problem of finite-horizon probabilistic invariance for discrete-time Markov processes over general (uncountable) state spaces. We compute discrete-time, finite-state Markov chains as formal abstractions of general Markov processes. Our abstraction differs from existing approaches in two ways. First, we exploit the structure of the underlying Markov process to compute the abstraction separately for each dimension. Second, we employ dynamic Bayesian networks (DBN) as compact representations of the abstraction. In contrast, existing approaches represent and store the (exponentially large) Markov chain explicitly, which leads to heavy memory requirements limiting the application to models of dimension less than half, according to our experiments. We show how to construct a DBN abstraction of a Markov process satisfying an independence assumption on the driving process noise. We compute a guaranteed bound on the error in the abstraction w.r.t. the probabilistic invariance property; the dimension-dependent abstraction makes the error bounds more precise than existing approaches. Additionally, we show how factor graphs and the sum-product algorithm for DBNs can be used to solve the finite-horizon probabilistic invariance problem. Together, DBN-based representations and algorithms can be significantly more efficient than explicit representations of Markov chains for abstracting and model checking structured Markov processes.
关键词：Structured stochastic systems; general space Markov processes; formal verification; dynamic Bayesian networks; Markov chain abstraction