SHAVE  Stochastic Hybrid Analysis of Markov Population Models
Subproject 
H4 
Categories 
Model checker for hard & soft realtime 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 momentbased and statebased 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 discretestate 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. 
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 

Manual 

Status 
Stable 