Reachability and reward checking for stochastic timed automata

E. Moritz Hahn, Arnd Hartmanns, Holger Hermanns

Research output: Contribution to journalArticleAcademicpeer-review

20 Citations (Scopus)
15 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
JournalEASST electronic communications
Publication statusPublished - 2014
Externally publishedYes
Event14th International Workshop on Automated Verification of Critical Systems, AVoCS 2014 - University of Twente, Enschede, Netherlands
Duration: 24 Sept 201426 Sept 2014
Conference number: 14


  • Expected rewards
  • Probabilistic reachability
  • Stochastic timed automata


Dive into the research topics of 'Reachability and reward checking for stochastic timed automata'. Together they form a unique fingerprint.

Cite this