SearcharxivSearch

arXiv subjects

Bahare Salmani

Publications and source records attributed to Bahare Salmani.

4 recordsLinked to original sources

Reasoning with Probabilities: Relating Weighted Model Counting and Probabilistic Model Checking

Weighted model counting (WMC) and probabilistic model checking (PMC) are two well- established frameworks that are independently developed, the former for probabilistic inference, the latter traditionally for probabilistic verification, though recently also applied to inference. The formal relationship between the two frameworks, however, remains largely unexplored. In this paper, we lay the foundations for how they relate: we present (1) a mapping from cycle- free parametric Markov chains (pMCs) to arithmetic circuits (ACs), enabling the reduction of reachability probability computations in such pMCs to a weighted model counting problem on the corresponding ACs, and (2) a mapping from a subclass of arithmetic circuits -- with probabilistic semantics -- back to parametric Markov chains. We propose a detailed correspondence between the entities of WMC and PMC, and discuss how our mappings enable transferring optimization techniques such as bisimulation minimization across the frameworks.

cs.LO

Finding an $ε$-close Variation of Parameters in Bayesian Networks

This paper addresses the $ε$-close parameter tuning problem for Bayesian Networks (BNs): find a minimal $ε$-close amendment of probability entries in a given set of (rows in) conditional probability tables that make a given quantitative constraint on the BN valid. Based on the state-of-the-art "region verification" techniques for parametric Markov chains, we propose an algorithm whose capabilities go beyond any existing techniques. Our experiments show that $ε$-close tuning of large BN benchmarks with up to 8 parameters is feasible. In particular, by allowing (i) varied parameters in multiple CPTs and (ii) inter-CPT parameter dependencies, we treat subclasses of parametric BNs that have received scant attention so far.

cs.AI

Fine-Tuning the Odds in Bayesian Networks

This paper proposes various new analysis techniques for Bayes networks in which conditional probability tables (CPTs) may contain symbolic variables. The key idea is to exploit scalable and powerful techniques for synthesis problems in parametric Markov chains. Our techniques are applicable to arbitrarily many, possibly dependent parameters that may occur in various CPTs. This lifts the severe restrictions on parameters, e.g., by restricting the number of parametrized CPTs to one or two, or by avoiding parameter dependencies between several CPTs, in existing works for parametric Bayes networks (pBNs). We describe how our techniques can be used for various pBN synthesis problems studied in the literature such as computing sensitivity functions (and values), simple and difference parameter tuning, ratio parameter tuning, and minimal change tuning. Experiments on several benchmarks show that our prototypical tool built on top of the probabilistic model checker Storm can handle several hundreds of parameters.

cs.AI

Bayesian Inference by Symbolic Model Checking

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.

cs.AI