Download User Manual

Chapter 12
Symbolic State Space Generator
The symbolic state space generator (symbolic SSG) is a component that was added to the Möbius
tool for version 1.6.0. In this chapter, we first introduce this component, discuss its advantages
and limitations, and describe how to use it in an efficient way. Then, we will explain how to fill
up each of the input parameters of its corresponding GUI editor. The different phases of the state
space generation will be briefly described. Finally, we will provide instructions on how to run the
symbolic SSG from the command line. For more details on the inner workings of the symbolic
SSG, please see [13, 14].
12.1
Introduction
In solving a model using numerical solution, a modeler must first run a state space generator on
the model to build a representation of the stochastic process underlying the model, and then use a
numerical solver to compute the measures (s)he is interested in.
A numerical solution algorithm needs data structures to represent two essential entities in the
memory: the stochastic process (input) and one or more probability distribution vectors (output).
The stochastic process is generated by a state space generator. In this chapter, we only consider
stochastic processes that are continuous time Markov chains (CTMCs), and can therefore be represented by state transition rate matrices whose entries are the rates of exponentially distributed timed
transitions from one state to another.
In many numerical solvers, sparse matrix representation and arrays are respectively used to
represent the process and the probability vector(s). In such a design of data structures, the stochastic
process represented by a sparse matrix almost always takes more memory space than the probability
vectors.
A problem arises when the model under study is so large that the memory requirement of the
two data structures exceeds the amount of memory available on a computer. For example, to analyze
a model with ten million states for a specific point of time using the transient solver (TRS) and the
123