Abstract
This paper applies probabilistic model checking techniques for discrete Markov chains to inference in Bayesian networks. We present a simple translation from Bayesian networks into tree-like Markov chains such that inference can be reduced to computing reachability probabilities. Using a prototypical implementation on top of the Storm model checker, we show that symbolic data structures such as multi-terminal BDDs (MTBDDs) are very effective to perform inference on large Bayesian network benchmarks. We compare our result to inference using probabilistic sentential decision diagrams and vtrees, a scalable symbolic technique in AI inference tools.
This work is funded by the ERC AdG Projekt FRAPPANT (Grant Nr. 787914).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Bayesian network Interchange Format. http://www.cs.washington.edu/dm/vfml/appendixes/bif.htm. Accessed 2019
de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 395–410. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46419-0_27
Bahar, R.I., et al.: Algebraic decision diagrams and their applications. Formal Methods Syst. Des. 10(2/3), 171–206 (1997)
Baier, C., Clarke, E.M., Hartonas-Garmhausen, V., Kwiatkowska, M., Ryan, M.: Symbolic model checking for probabilistic processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 430–440. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63165-8_199
Baier, C., Klein, J., Klüppelholz, S., Märcker, S.: Computing conditional probabilities in Markovian models efficiently. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 515–530. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_43
Batz, K., Kaminski, B.L., Katoen, J.-P., Matheja, C.: How long, O Bayesian network, will I sample thee? In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 186–213. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89884-1_7
Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45(9), 993–1002 (1996)
Bryant, R.E.: Binary decision diagrams. Handbook of Model Checking, pp. 191–217. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_7
Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: quantitative model and tool interaction. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 151–168. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54580-5_9
Chaki, S., Gurfinkel, A.: BDD-based symbolic model checking. Handbook of Model Checking, pp. 219–245. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-10575-8_8
Chavira, M., Darwiche, A.: Compiling Bayesian networks with local structure. In: IJCAI, pp. 1306–1312. Professional Book Center (2005)
Chavira, M., Darwiche, A., Jaeger, M.: Compiling relational Bayesian networks for exact inference. Int. J. Approx. Reason. 42(1–2), 4–20 (2006)
Cooper, G.F.: The computational complexity of probabilistic inference using Bayesian belief networks. Artif. Intell. 42(2–3), 393–405 (1990)
Dagum, P., Luby, M.: Approximating probabilistic inference in Bayesian belief networks is NP-Hard. Artif. Intell. 60(1), 141–153 (1993)
Darwiche, A.: A logical approach to factoring belief networks. In: KR, pp. 409–420. Morgan Kaufmann (2002)
Darwiche, A.: New advances in compiling CNF into Decomposable Negation Normal Form. In: ECAI, pp. 328–332. IOS Press (2004)
Darwiche, A.: Modeling and Reasoning with Bayesian Networks. Cambridge University Press, Cambridge (2009)
Darwiche, A.: SDD: a new canonical representation of propositional knowledge bases. In: IJCAI, pp. 819–826. IJCAI/AAAI (2011)
Darwiche, A.: A differential approach to inference in Bayesian networks. CoRR abs/1301.3847 (2013)
Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A STORM is coming: a modern probabilistic model checker. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592–600. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_31
Deininger, D., Dimitrova, R., Majumdar, R.: Symbolic model checking for factored probabilistic models. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 444–460. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46520-3_28
Fujita, M., McGeer, P.C., Yang, J.C.: Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Formal Methods Syst. Des. 10(2/3), 149–169 (1997)
Gehr, T., Misailovic, S., Vechev, M.: PSI: exact symbolic inference for probabilistic programs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 62–83. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_4
Hahn, E.M., et al.: The 2019 comparison of tools for the analysis of quantitative formal models. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 69–92. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17502-3_5
Holtzen, S., Millstein, T.D., Van den Broeck, G.: Symbolic exact inference for discrete probabilistic programs. CoRR abs/1904.02079 (2019)
Hopkins, M., Darwiche, A.: A practical relaxation of constant-factor treewidth approximation algorithms. In: Proceedings of the First European Workshop on Probabilistic Graphical Models. PGM, pp. 71–80. Citeseer (2002)
Jaeger, M.: Complex probabilistic modeling with recursive relational Bayesian networks. Ann. Math. Artif. Intell. 32(1–4), 179–220 (2001)
Jensen, F.V.: Bayesian Networks and Decision Graphs. Statistics for Engineering and Information Science. Springer, New York (2001). https://doi.org/10.1007/978-1-4757-3502-4
Katoen, J.: The probabilistic model checking landscape. In: LICS, pp. 31–45. ACM (2016)
Kisa, D., Van den Broeck, G., Choi, A., Darwiche, A.: Probabilistic sentential decision diagrams. In: KR. AAAI Press (2014)
Klein, J., et al.: Advances in symbolic probabilistic model checking with PRISM. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 349–366. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_20
Koller, D., Friedman, N.: Probabilistic Graphical Models - Principles and Techniques. MIT Press, Cambridge (2009)
Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_47
Langmead, C., Jha, S., Clarke, E.: Temporal logics as query languages for dynamic Bayesian networks: application to d. melanogaster embryo development. Technical report, Carnegie Mellon University (2006)
Langmead, C.J.: Towards inference and learning in dynamic Bayesian networks using generalized evidence. Technical report, Carnegie Mellon University (2008)
Minato, S., Satoh, K., Sato, T.: Compiling Bayesian networks by symbolic probability calculation based on zero-suppressed BDDs. In: IJCAI, pp. 2550–2555 (2007)
Palaniappan, S.K., Thiagarajan, P.S.: Dynamic Bayesian networks: a factored model of probabilistic dynamics. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 17–25. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33386-6_2
Pipatsrisawat, K., Darwiche, A.: New compilation languages based on structured decomposability. In: AAAI, pp. 517–522. AAAI Press (2008)
Pipatsrisawat, T., Darwiche, A.: A lower bound on the size of decomposable negation normal form. In: AAAI. AAAI Press (2010)
Sanner, S., McAllester, D.A.: Affine algebraic decision diagrams (AADDs) and their application to structured probabilistic inference. In: IJCAI, pp. 1384–1390. Professional Book Center (2005)
Scutari, M.: Bayesian network repository. https://www.bnlearn.com. Accessed 2019
Shachter, R.D., D’Ambrosio, B., Favero, B.D.: Symbolic probabilistic inference in belief networks. In: AAAI, pp. 126–131. AAAI Press/The MIT Press (1990)
Shih, A., Choi, A., Darwiche, A.: Formal verification of Bayesian network classifiers. In: Proceedings of Machine Learning Research. PGM, vol. 72, pp. 427–438. PMLR (2018)
Xue, Y., Choi, A., Darwiche, A.: Basing decisions on sentences in decision diagrams. In: AAAI. AAAI Press (2012)
Acknowledgement
The authors would like to thank Yujia Shen (UCLA) for his kind support with running the PSDD tools.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Salmani, B., Katoen, JP. (2020). Bayesian Inference by Symbolic Model Checking. In: Gribaudo, M., Jansen, D.N., Remke, A. (eds) Quantitative Evaluation of Systems. QEST 2020. Lecture Notes in Computer Science(), vol 12289. Springer, Cham. https://doi.org/10.1007/978-3-030-59854-9_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-59854-9_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-59853-2
Online ISBN: 978-3-030-59854-9
eBook Packages: Computer ScienceComputer Science (R0)