From stochastic automata to timed automata: Abstracting probability in a compositional manner

Abstract. We present a translation from stochastic automata [10, 8] into timed automata with deadlines [5]. The translation abstracts prob-abilities and preserves trace behaviour. Moreover, it is compositional in the sense that the translation of the parallel composition of two stochastic automata is equivalent to the parallel composition of the timed automata resulting from the translation of each component.