Probabilistic reasoning is a key to handling uncertainties and making decisions based on partial observations. Bayesian networks (BNs) are popular probabilistic graphical models in probabilistic decision-making and AI and have a wide range of applications, including machine learning, medicine, gene regulatory networks, and robotics. They combine the notions from probability theory and graph theory and enable a succinct representation of joint probability distributions. A Bayesian network is composed of a directed acyclic graph over a set of random variables and a set of conditional probability tables ---CPTs for short. The primary task in Bayesian networks is probabilistic inference, that is, to compute a conditional probability of a joint valuation for a subset of random variables given an observation.

Probabilistic model checking is a field in computer science that is focused on analyzing stochastic systems with respect to a set of formally defined properties. The stochastic systems are typically Markov models, and the properties of interest are probabilistic extensions of LTL of CTL.  The properties are mostly reduced to a pivotal task, computing reachability probabilities: what is the probability of reaching a set of target states? Recent advancements in the field consider the parametric extensions of the Markov models, where a subset of the probabilities in the model are unknown and target various synthesis problems including feasibility checking: is there a satisfying instantiation that satisfies the given constraint?, region verification: are all instantiations in a region satisfy the given constraint, and parameter space partitioning: split the entire n-dimensional parameter space to sets of satisfying, rejecting, and unknown subregions w.r.t. the given constraint.

In this dissertation, we present a new approach based on probabilistic model checking for inference and parameter tuning in Bayesian networks. The dissertation is categorized into two main settings: the non-parametric and the parametric. In the non-parametric setting, we focus on the classical Bayesian networks, where the model is fully specified. We present mappings from Bayesian networks to discrete-time Markov chains and mathematically reduce performing conditional inference in the BN to computing reachability probabilities in Markov chains. This enables the use of state-of-the-art algorithms for computing reachability probabilities and the optimization techniques thereof, e.g., bisimulation minimization for exact inference in BNs. We exploit the explicit and symbolic methods from probabilistic model checking and empirically evaluate our framework for Bayesian inference against the state-of-the-art weighted model counting. In the parametric setting, we define parametric Bayesian networks (pBNs), where a subset of CPT entries are unknown polynomials rather than concrete probabilities. We build upon the synthesis techniques for parametric Markov chains and address problems sensitivity analysis, ratio/difference parameter tuning from the BN literature, and parameter space partitioning from pMC literature. Finally, we focus on the problem minimal-distance parameter tuning, where the objective is to find the instantiation u for the unknown parameters that satisfy the constraint of interest while minimally deviating from the original instantiation u_0 in an original reference model. The motivation is to minimally disturb the statistical information in the original model. 

 

Our detailed experimental evaluations indicate that our parameter synthesis techniques can treat parameter synthesis for Bayesian networks (with hundreds of unknown parameters) that go beyond the capabilities of the existing techniques. We lift the severe restrictions in the literature on the number of unknown parameters, the global dependencies between the parameters, and the form of obtained solutions.

---