T3: Structured analysis of Markov chains
  This tutorial consists of two parts:
Structured Analysis of Markov Models:
Peter Buchholz
(Univ. of Dortmund, Germany)
Duration: 90 minutes
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
Markov chains are a powerful and conceptually easy class of discrete-state 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 continuous-time Markov chain. Then, we examine numerical solution algorithms that operate on these encodings.
Web Maintenance Person.