Measuring performance of continuous-time stochastic processes using timed automata

Tomáš Brázdil, Jan Krčál, Jan Křetínský, Antonín Kučera, Vojtěch Řehák

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

5 Scopus citations

Abstract

We propose deterministic timed automata (DTA) as a model-independent language for specifying performance and dependability measures over continuous-time stochastic processes. Technically, these measures are defined as limit frequencies of locations (control states) of a DTA that observes computations of a given stochastic process. Then, we study the properties of DTA measures over semi-Markov processes in greater detail. We show that DTA measures over semi-Markov processes are well-defined with probability one, and there are only finitely many values that can be assumed by these measures with positive probability. We also give an algorithm which approximates these values and the associated probabilities up to an arbitrarily small given precision. Thus, we obtain a general and effective framework for analysing DTA measures over semi-Markov processes.

Original languageEnglish
Title of host publicationHSCC'11 - Proceedings of the 2011 ACM/SIGBED Hybrid Systems
Subtitle of host publicationComputation and Control
Pages33-42
Number of pages10
DOIs
StatePublished - 2011
Externally publishedYes
Event14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011 - Chicago, IL, United States
Duration: 12 Apr 201114 Apr 2011

Publication series

NameHSCC'11 - Proceedings of the 2011 ACM/SIGBED Hybrid Systems: Computation and Control

Conference

Conference14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011
Country/TerritoryUnited States
CityChicago, IL
Period12/04/1114/04/11

Keywords

  • General state space Markov chains
  • Performance analysis
  • Semi-Markov processes
  • Stochastic stability
  • Timed automata

Fingerprint

Dive into the research topics of 'Measuring performance of continuous-time stochastic processes using timed automata'. Together they form a unique fingerprint.

Cite this