SHAVE - Stochastic Hybrid Analysis of Markov Population Models

 

Subproject

H4

Categories

Model checker for hard & soft real-time systems, Model checker / solver for probabilistic systems

Overview

SHAVE is a tool for the stochastic hybrid analysis of Markov population models, that is, Markov processes with an underlying population structure. It efficiently computes an accurate approximation of the probability distribution at a particular time instant based on a stochastic hybrid model that combines moment-based and state-based representations of probability distributions.

SHAVE is primarily used to analyze networks of chemical reactions as they are of interest in the systems biology domain but SHAVE is not restricted to those. In fact, SHAVE can analyze any discrete-state Markov process whose transitions can be partitioned into a finite number of classes (e.g. "birth" and "death" of objects of a certain type). SHAVE models can be specified using a simple language.

Publications

M. Lapin, L. Mikeev, and V. Wolf. SHAVE - Stochastic Hybrid Analysis of Markov Population Models. In Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control (HSCC), 2011.

Benchmarks

---

Download

See alma.cs.uni-saarland.de/shave/

Manual

See alma.cs.uni-saarland.de/shave/

Status

Stable