bb

 

Subproject

S3

Categories

Systems of systems / blackbox tools, Model checker / solver for probabilistic systems

Overview

The purpose of the bb tool is to compute bounds on the probability of reaching a set of target states in an incomplete network of Markov decision processes (MDPs). Incomplete means that the internal structure of some of the components of the network is not available but only the interface via which they communicate with the available parts.

Publications

R. Wimmer, E.M. Hahn, H. Hermanns, and B. Becker. Reachability analysis for incomplete networks of Markov decision processes. In Barbara Jobstmann and Michael Kishinevsky, editors, Proceedings of the ACM/IEEE 9th International Conference on Formal Methods and Models for Codesign (MEMOCODE), 2011.

Benchmarks

Chord Network

Download

Click here for the binary.

Manual

Just type ./bb on the command line to see how it can be used.

Status

Prototype