Model Checking for Probabilistic Timed Systems

Application areas such as multimedia equipment, communication protocols and networks often feature systems which exhibit both probabilistic and timed behaviour. In this paper, we consider analysis of such probabilistic timed systems using the technique of model checking, in which it is verified automatically whether a system satisfies a certain desired property. In order to describe formally probabilistic timed systems, we consider probabilistic extensions of timed automata, such as real-time probabilistic processes, probabilistic timed automata and continuous probabilistic timed automata, the underlying semantics of each of which is an infinite-state structure. For each formalism, we consider how the well-known region equivalence relation can be used to reduce the infinite state-space model into a finite-state system, which can then be used for model checking.