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.

Publications

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

See alma.cs.uni-saarland.de

Manual

See alma.cs.uni-saarland.de

Status

Stable