License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2015.169
URN: urn:nbn:de:0030-drops-53693
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5369/
Go to the corresponding LIPIcs Volume Portal

Esmaeil Zadeh Soudjani, Sadegh ; Abate, Alessandro ; Majumdar, Rupak

Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes

pdf-format:
9.pdf (0.5 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{esmaeilzadehsoudjani_et_al:LIPIcs:2015:5369,
  author =	{Sadegh Esmaeil Zadeh Soudjani and Alessandro Abate and Rupak Majumdar},
  title =	{{Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{169--183},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Luca Aceto and David de Frutos Escrig},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5369},
  URN =		{urn:nbn:de:0030-drops-53693},
  doi =		{10.4230/LIPIcs.CONCUR.2015.169},
  annote =	{Keywords: Structured stochastic systems, general space Markov processes, formal verification, dynamic Bayesian networks, Markov chain abstraction}
}

Keywords: Structured stochastic systems, general space Markov processes, formal verification, dynamic Bayesian networks, Markov chain abstraction
Collection: 26th International Conference on Concurrency Theory (CONCUR 2015)
Issue Date: 2015
Date of publication: 26.08.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI