Bayesian inference by symbolic model checking

DOI10.1007/978-3-030-59854-9_9zbMATH Open1483.68204arXiv2007.15071OpenAlexW3109856706MaRDI QIDQ2056985FDOQ2056985

Authors: Bahare Salmani, Joost-Pieter Katoen 

Publication date: 8 December 2021

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.

Full work available at URL: https://arxiv.org/abs/2007.15071

Recommendations

• Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference
• Symbolic model checking for factored probabilistic models
• Modeling and Reasoning with Bayesian Networks
• Model checking finite-horizon Markov chains with probabilistic inference
• scientific article; zbMATH DE number 2096817

Mathematics Subject Classification ID

Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Probabilistic graphical models (62H22) Reasoning under uncertainty in the context of artificial intelligence (68T37) Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (13)

• Model checking finite-horizon Markov chains with probabilistic inference
• Probabilistic Model Checking for Continuous-Time Markov Chains via Sequential Bayesian Inference
• Reachability design through approximate Bayesian computation
• Symbolic model checking for factored probabilistic models
• Bayesian statistical model checking with application to Stateflow/Simulink verification
• How long, O Bayesian network, will I sample thee? A program analysis perspective on expected sampling times
• Fine-tuning the odds in Bayesian networks
• Gradient-descent for randomized controllers under partial observability
• Automatically finding the right probabilities in Bayesian networks
• Computational Science – ICCS 2005
• Exact Bayesian inference by symbolic disintegration
• State-space abstractions for probabilistic inference: a systematic review
• Dynamic Bayesian networks for formal verification of structured stochastic processes

This page was built for publication: Bayesian inference by symbolic model checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2056985)