Traditionally, in verification models there have been no quantitative measures associated with system behaviours. However for the purpose of optimisation one needs to compare behaviours (or sets of behaviours) quantitatively in order to prefer one controller over the other. First steps in this direction have been done by consortium members who associated time duration and costs with the runs of a timed automaton. The consortium intends to investigate to what extent these models are suitable for the class of applications under consideration and whether they can be extended while maintaining the analysis tractable.

A more important quantitative aspect is manifested when one moves to stochastic models. In many situations real-time description of systems, their environments and requirements are given in stochastic rather than absolute terms. For example, in some cases the arrival times of new jobs may be best characterised by a certain probability distribution instead of a single, guaranteed maximal arrival time. Likewise, a system might be expected to miss deadlines in very a small probability, rather than not to miss it at all. Studying the functional correctness of such systems is very closely linked to performance analysis. For many modern applications, such as multi-media network protocols and more generally the class of ``soft'' real-time systems it is in fact impossible to separate functional correctness from performance in the form of guaranteed quality-of-service (QoS).

The purpose of this task is to study and develop stochastic extensions of the basic model of timed automata emphasising their specification and composition. The conceptual problems posed by this task are rather subtle because currently the semantics of timed automata consists of sets of continuous time behaviour, while in a stochastic setting the behaviour is a continuous time evolution of a probability distribution over the state-space as, for example in continuous-time Markov chains. It is expected that the definition of a stochastic delay operator and its composition with logical elements will lead to models much richer than traditional models; it will be a significant challenge to develop tractable analysis methods for them.

responsible partner: UTWENTE