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.
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.
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.
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.
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.
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 the 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.
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.
The established continuous stochastic logic (CSL) allows to express properties of MPMs, such as probabilistic reachability, survivability, oscillations, switching times between attractor regions, and various others. GeoInf combines the tools Geobound and Infamy to handle complete CSL for MPMs.
For a complete description of the used algorithms we refer to our technical report “A CSL Model Checker for Markov Population Models” on arXiv.org.
The GeoInf tool chain is based on two tools called Geobound and Infamy that were slightly extended in order to communicate with each other, i.e. Infamy is used to do the model checking and transient analysis while Geobound provides the steady state analysis.
Notice: The tools were built on and should be run on recent versions of (for instance, Ubuntu) Linux.
More information about Infamy can be found on the Infamy tool homepage.
Please download both tools and modify the parameters in the shell scripts shipped along the case studies accordingly to the place where the tools reside. Then, run the shell scripts.
Authors: Geobound was written by David Spieler. Infamy was written by Ernst Moritz Hahn.