Geobound
Subproject |
S3 |
Categories |
Model checker / solver for probabilistic systems |
Overview |
Geobound takes a structured infinite state CTMC (Markov population model) and utilizes Lyapunov functions together with geometric bounding techniques to retrieve a state space window that encloses a major part of the steady state probability mass. In a followed-up analysis step, Geobound also computes state-wise bounds on the equilibrium distribution inside that window. |
T. Dayar, H. Hermanns, D. Spieler, and V Wolf. Bounding the equilibrium distribution of markov population models. Numerical Linear Algebra with Applications, 2011. Accepted for publication. |
|
Benchmarks |
--- |
Download |
|
Manual |
|
Status |
Stable |