Reachability and Reward Checking for Stochastic Timed Automata

Ernst Moritz Hahn, Arnd Hartmanns, Holger Hermanns

Research output: Contribution to journalArticlepeer-review

20 Citations (Scopus)
30 Downloads (Pure)


Stochastic timed automata are an expressive formal model for hard and soft real-time systems. They support choices and delays that can be deterministic, nondeterministic or stochastic. Stochastic choices and delays can be based on arbitrary discrete and continuous distributions. In this paper, we present an analysis approach for stochastic timed automata based on abstraction and probabilistic model checking. It delivers upper/lower bounds on maximum/minimum reachability probabilities and expected cumulative reward values. Based on theory originally developed for stochastic hybrid systems, it is the first fully automated model checking technique for stochastic timed automata. Using an implementation as part of the Modest Toolset and four varied examples, we show that the approach works in practice and present a detailed evaluation of its applicability, its efficiency, and current limitations.
Original languageEnglish
Number of pages15
Publication statusPublished - 2014


Dive into the research topics of 'Reachability and Reward Checking for Stochastic Timed Automata'. Together they form a unique fingerprint.

Cite this