The 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 task.

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.

responsible partner: UT