
Structured Analysis of Markov Models: 
Peter Buchholz
(Univ. of Dortmund, Germany)

Duration: 90 minutes 
ABSTRACT:
Markov models are a commonly used model type to analyze all kinds of
systems. Although the general approach of generating Markov chains
from high level specifications and of analyzing the resulting Markov
chain are well understood and easy to realize, practical problems occur
due the so called state space explosion which means that the size of
the state space of the Markov chain grows exponentially with the size
of the model.
Recently a remarkable step forward has been made in generating and
storing huge state space and transition matrices with 10^20 states
and beyond using advanced data structures. Based on these representations
functional properties of the system can be analyzed. Additionally,
these compact storage schemes have been used for quantitative analysis
via numerical computation of the stationary or transient distribution.
However, although the new techniques enlarge the size of solvable state
spaces significantly, the size is limited by the size of the probability
vector which allows the analysis of systems with 10^7 states, but not
with 10^20 states. Thus, new approachs are required which avoid storing
all states and still allow the computation of quantitative results.
The tutorial gives an overview of different recently developed approaches
which exploit the compact representation of the whole states space for
quantitative analysis without storing the whole vector of state
probabilities. In particular
 approximation techniques based on fixed point computations,
 bounding techniques, and
 hybrid techniques combining simulation and transient numerical analysis
are presented and compared. Furthermore, it is outlined how these
techniques can be integrated in software tools for performance
analysis and which research problems are currently open.
 

Modeling and Analysis of Markov Chains Using Decision Diagrams 
Gianfranco Ciardo
(Univ. of California at Riverside, USA)

Duration: 90 minutes 
ABSTRACT:
Markov chains are a powerful and conceptually easy class of
discretestate stochastic processes that can be used to model
a wide variety of systems. However, high modeling fidelity
is often achieved only when the state space of the Markov chain
is very large, making the numerical solution of these models
a formidable task. In this tutorial, we review and compare
several techniques to encode a very large matrix, such as
the transition rate matrix of a continuoustime Markov chain.
Then, we examine numerical solution algorithms that operate
on these encodings.
 