various extensions of the timed automata paradigm to a stochastic setting lead
to a wide range of models that include features from discrete and continuous
Markov chains, Markov decision processes, stochastic discrete event systems,
etc. The challenge is to combine techniques for timed automata verification
with those for performance analysis into effective, integrated methods for analysing
such hybrid models. In particular, the traditional techniques for dealing with
large stochastic systems (e.g. sparse matrices, Kronecker representation, linear
programming, MTBDDs, ADDs, PDGs) must be combined with efficient data structures
for symbolic manipulation of timed automata models (e.g. DBMs, CDDs, DDDs, NDDs).
Current work on applying compositional and model checking techniques for the
analysis of various Markovian models is a good starting for the work in this
The consortium aims at combining tools currently developed by members of
the consortium for model checking and performance analysis of purely Markovian
models with existing real-time verification tools.