Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes

Authors Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate, Rupak Majumdar

Thumbnail PDF


  • Filesize: 0.52 MB
  • 15 pages

Document Identifiers

Author Details

Sadegh Esmaeil Zadeh Soudjani
Alessandro Abate
Rupak Majumdar

Cite AsGet BibTex

Sadegh Esmaeil Zadeh Soudjani, Alessandro Abate, and Rupak Majumdar. Dynamic Bayesian Networks as Formal Abstractions of Structured Stochastic Processes. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 169-183, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


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


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. A. Abate, J.-P. Katoen, J. Lygeros, and M. Prandini. Approximate model checking of stochastic hybrid systems. European Journal of Control, 6:624-641, 2010. Google Scholar
  2. A. Abate, M. Prandini, J. Lygeros, and S. Sastry. Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica, 44(11):2724-2734, 2008. Google Scholar
  3. A. Abate, S. Vincent, R. Dobbe, A. Silletti, N. Master, J. Axelrod, and C.J. Tomlin. A mechanical modeling framework for the study of epithelial morphogenesis. IEEE/ACM Transactions on Computational Biology and Bioinformatics, 9(6):1607-1620, Nov 2012. Google Scholar
  4. J. Angeles. Dynamic Response of Linear Mechanical Systems - Modeling, Analysis and Simulation. Springer US, 2012. Google Scholar
  5. C. Baier and J.-P. Katoen. Principles of Model Checking. MIT Press, 2008. Google Scholar
  6. D.P. Bertsekas. Convergence of discretization procedures in dynamic programming. IEEE Transactions on Automatic Control, 20(3):415-419, 1975. Google Scholar
  7. S. Esmaeil Zadeh Soudjani and A. Abate. Adaptive gridding for abstraction and verification of stochastic hybrid systems. In QEST, pages 59-69, 2011. Google Scholar
  8. S. Esmaeil Zadeh Soudjani and A. Abate. Adaptive and sequential gridding procedures for the abstraction and verification of stochastic processes. SIAM Journal on Applied Dynamical Systems, 12(2):921-956, 2013. Google Scholar
  9. S. Esmaeil Zadeh Soudjani, A. Abate, and R. Majumdar. Dynamic bayesian networks as formal abstractions of structured stochastic processes. 26th Conference on Concurrency Theory, 2015. arXiv:1507.00509. Google Scholar
  10. S. Esmaeil Zadeh Soudjani, C. Gevaerts, and A. Abate. FAUST^2: Formal abstractions of uncountable-state stochastic processes. In TACAS, volume 9035 of LNCS, pages 272-286. Springer, 2015. Google Scholar
  11. A. Gusrialdi and S. Hirche. Communication topology design for large-scale interconnected systems with time delay. In American Control Conference, pages 4508-4513, June 2011. Google Scholar
  12. S.K. Jha, E.M. Clarke, C.J. Langmead, A. Legay, A. Platzer, and P. Zuliani. A Bayesian approach to model checking biological systems. In Computational Methods in Systems Biology, volume 5688 of LNCS, pages 218-234. Springer, 2009. Google Scholar
  13. O. Kallenberg. Foundations of Modern Probability. Probability and its Applications. Springer Verlag, New York, 2002. Google Scholar
  14. J.-P. Katoen, M. Khattri, and I. S. Zapreev. A Markov reward model checker. In QEST, pages 243-244. IEEE, 2005. Google Scholar
  15. D. Koller and N. Friedman. Probabilistic Graphical Models: Principles and Techniques - Adaptive Computation and Machine Learning. The MIT Press, 2009. Google Scholar
  16. L.Y. Kolotilina. Bounds for the singular values of a matrix involving its sparsity pattern. Journal of Mathematical Sciences, 137(3):4794-4800, 2006. Google Scholar
  17. F.R. Kschischang, B.J. Frey, and H.-A. Loeliger. Factor graphs and the sum-product algorithm. IEEE Transactions on Information Theory, 47(2):498-519, 2001. Google Scholar
  18. M. Kwiatkowska, G. Norman, and D. Parker. PRISM 4.0: Verification of probabilistic real-time systems. In CAV, volume 6806 of LNCS, pages 585-591. Springer, 2011. Google Scholar
  19. C.J. Langmead. Generalized queries and Bayesian statistical model checking in dynamic Bayesian networks: Application to personalized medicine. In Proc. 8th International Conference on Computational Systems Bioinformatics, pages 201-212, 2009. Google Scholar
  20. K.P. Murphy. Dynamic Bayesian Networks: Representation, Inference and Learning. PhD thesis, UC Berkeley, Computer Science Division, 2002. Google Scholar
  21. S.K. Palaniappan and P.S. Thiagarajan. Dynamic Bayesian networks: A factored model of probabilistic dynamics. In ATVA, volume 7561 of LNCS, pages 17-25. Springer, 2012. Google Scholar
  22. F. Ramponi, D. Chatterjee, S. Summers, and J. Lygeros. On the connections between PCTL and dynamic programming. In HSCC, pages 253-262, 2010. Google Scholar
  23. V. Sundarapandian. Distributed control schemes for large-scale interconnected discrete-time linear systems. Mathematical and Computer Modelling, 41(2–3):313-319, 2005. Google Scholar
  24. I. Tkachev and A. Abate. Formula-free finite abstractions for linear temporal verification of stochastic hybrid systems. In HSCC, pages 283-292, 2013. Google Scholar
  25. I. Tkachev, A. Mereacre, J.-P. Katoen, and A. Abate. Quantitative automata-based controller synthesis for non-autonomous stochastic hybrid systems. In HSCC, pages 293-302, 2013. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail