Geobound

Overview

Update: The GeoInf (Geobound + Infamy) tool homepage can be found here.

Continuous-time Markov chains (CTMC) are a widely used modelling formalism for systems when probabilistic and timed behavior is of interest. Often, the equilibrium distribution of CTMC can be vital for showing properties about the underlying systems. Many examples can be found in queuing theory and systems biology. So far the models that could be analzed were limited, i.e. the underlying state-space either was finite or the transitions of states had to follow a very restricted pattern. Our tool, Geobound, allows for a more general class of infinite state CTMC, i.e. systems induced by sets of transition classes. The tool first utilizes Lyapunov functions and geometric bounding techniques to retrieve a window inside the state space that encloses a major part of the steady state probability mass and then does a more detailed analysis inside that window revealing even state-wise bounds on the equilibrium distribution.

Methodology

In a nutshell, Geobound takes a transition class model and a polynomial Lyapunov function as input and symbolically computes the drift, i.e. a multivariate polynomial expressing the expected change in the Lyapunov function for each state.

Geometric bounds: In order to retrieve a window, i.e. a finite subset of the typically infinite state space, that contains at least 1-epsilon of the steady-state probability mass, Geobound scales the drift by that epsilon and the global maximum drift and exploits results by Tweedie [1] that allow the retrieval of the desired window by taking exactly those states that exceed a certain scaled drift value.

Geometric Bounds

Exclusive switch – geometric bounds.

State-wise bounds: In a second analysis step, Geobound computes state-wise bounds on the equilibrium distribution. For that, results by Courtois and Semal [2] are used to retrieve bounds on the steady-state distriubution inside that window conditioned on that window.

Bounds Min

Exclusive switch – lower bounds.

Bounds Diff

Exclusive switch – difference between upper and lower bounds.

A more detailed description on the methodology used to retrieve the geometric bounds as well as the state-wise bounds on the equilibrium distribution can be found in this technical report [3]. Geobound uses HOM4PS-2.0 [4] to solve the systems of non-linear equations that emerge when computing the global maximum drift and the SuperLU package in order to compute the state wise bounds.

Download

The current version of Geobound is 0.3.3 and is distributed as a pre-built package for Linux 32-bit and comes with HOM4PS2 included.

Please follow the installation steps as described in the readme file and make sure that the Java 6 runtime and the Fortran to C (libf2c) library is installed on your system.

Download: Pre-built 32-bit Linux Version

References

[1] Richard L. Tweedie. Sufficient conditions for regularity, recurrence and ergodicity of markov processes. Mathematical Proceedings of the Cambridge Philosophical Society, 78(01):125–136, 1975.

[2] P.-J. Courtois and P. Semal. Bounds for the positive eigenvectors of nonnegative matrices and for their approximations by decomposition. J. ACM, 31(4):804–825, 1984.

[3] arXiv:1007.3130v1 [math.PR]

[4] T. L. Lee, T. Y. Li, and C. H. Tsai. Hom4ps-2.0: a software package for solving polynomial systems by the polyhedral homotopy continuation method. Computing, 83(2-3):109–133, 2008.