Commit 20ba776e authored by Hans Vrapi's avatar Hans Vrapi
Browse files

update file

parent d48a1863
# Storm-bn
Storm-bn s a prototypical tool for the analysis of (parametric) Bayesian networks. It presents alternative techniques for (a) inference on classical Bayesian networks in which all probabilities are fixed, and for (b) parameter synthesis problems when conditional probability tables (CPTs) in such networks contain symbolic variables rather than concrete probabilities. The key idea is to exploit probabilistic model checking as well as its recent extension to parameter synthesis techniques thereof for parametric Markov chains. To enable this, the (parametric) Bayesian networks are transformed into (parametric) Markov chains and their objectives are mapped onto probabilistic temporal logic formulas (PCTL).
(a) Given the Bayesian network B (and the evidence E), our tool-chain enables computing the inference probabilities for the given queries.
[![Build Status](](
(b) Given the parametric Bayesian network (pBN) B (and the evidence E), it enables
This repository facilitates performing tasks related to inference in parametric Bayesian networks (pBNs) such as:
- Feasibility Analysis
- Parameter Space Partitioning
- Sensitivity Analysis
- computing the sensitivity functions (and values) for a given query
by means of probabilistic model checking techniques. For this purpose, we have implemented the tool 'storm-bn-refactoring' that transforms a (parametric) Bayesian network (pBN) to their [corresponding] (parametric) Markov Chain (pMC). The generated pMC is fed into the probabilsitic model checker [Storm] to perform the computations for each of the mentioned tasks.
- synthesizing and tuning the parameters with respect to a given constraint, i.e., finding a single parameter instantiation that satisfies the constraint.
## Requirements
- partitioning the entire n-dimensional parameter space of the pBN into satisfying, rejecting, and --with some approximation factor- unknown regions for a given query and a given coverage factor, i.e., it provides the thorough information: which parameters instantiations satisfy and which violate the constraint.
- [Storm] 1.6.4
- [Prophesy]
- [bn-mc-transformer]
Storm-bn parameter synthesis features are applicable to arbitrarily many, possibly dependent, parameters that may occur in multiple CPTs. This lifts restrictions, e.g., on the number of parametrized CPTs, or on parameter dependencies between several CPTs, that exist in the existing pBN analysis tools.
## Booting the Docker image
To access the tool easier, download the Docker image and open it using docker software. We have tested everything using 8GB of RAM.
This work has been done at RWTH Aachen University.
[Storm]: <>
[Prophesy]: <>
[corresponding]: <>
[bn-mc-transformer]: <>
##Subdirectories Description:
Storm-bn-transformer: this is the (p)BN2(p)MC transformer on top of Storm that takes (parametric) Bayesian networks in BIF format and translates them into the Jani specification.
The package supports two types of translations:
The evidence-agnostic translation: it takes the (p)BN and translates it to a (p)MC.
The evidence-tailored translation: it takes the (p)BN + evidence E (+ hypothesis H), and creates a succincter (p)MC that also takes evidence E into account.
auxilary_scripts: this package includes the scripts for parameterizing the networks.
ace_storm_comparison: this subdirectory includes the experiments that compare Storm and Ace in probabilistic inference on classical BNs.
psdd_storm_comparison: this subdirectory includes the experiments that compare psdd_package and Storm in performing symbolic probabilistic inference on classical BNs.
storm_evidence: this directory includes the experiments that compare our evidence-agnostic and evidence-tailored translation in performing probabilistic inference on BNs.
sensitivity_analysis: this subdirectory includes the experiments that compare Storm and Bayesserver in computing the sensitivity functions for pBNs.
feasibility_analysis: this subdirectory includes the experiments that perform parameter tuning on pBNs using the state-of-the-art feasibility checking techniques for parametric Markov chains. The experiments compare the methods of "Particle Swarm Optimization", and "Quadratically-Constrained Quadratic Program (QCQP), and Gradient-Descent (GD) for this task.
parameters_space_paritioning: this subdirectory contains all the experiments for pBN partitioning using the parameter lifting algorithm.
We took benchmarks from Bayesian network repository: bnlearn. The (parameteric) benchmarks and the query files for all the experiments are accessible in the corresponding subdirectories.
Storm: the backend probabilistic model checker and the parameter synthesis tools for the tasks "sensitivity function computation", "parameter space partitioning", and "feasibility analysis: gradient-descent"
Prophesy: the backend parameter synthesis tool for feasibility analysis: QCQP and PSO.
Principle developer:
Bahare Salmani (contact point: salmani at
Robin Drahovskey
Caroline Jabs
David Korzeniewski
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment