TY - GEN
T1 - Measuring performance of continuous-time stochastic processes using timed automata
AU - Brázdil, Tomáš
AU - Krčál, Jan
AU - Křetínský, Jan
AU - Kučera, Antonín
AU - Řehák, Vojtěch
PY - 2011
Y1 - 2011
N2 - 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.
AB - 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.
KW - General state space Markov chains
KW - Performance analysis
KW - Semi-Markov processes
KW - Stochastic stability
KW - Timed automata
UR - http://www.scopus.com/inward/record.url?scp=79956038046&partnerID=8YFLogxK
U2 - 10.1145/1967701.1967709
DO - 10.1145/1967701.1967709
M3 - Conference contribution
AN - SCOPUS:79956038046
SN - 9781450306294
T3 - HSCC'11 - Proceedings of the 2011 ACM/SIGBED Hybrid Systems: Computation and Control
SP - 33
EP - 42
BT - HSCC'11 - Proceedings of the 2011 ACM/SIGBED Hybrid Systems
T2 - 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011
Y2 - 12 April 2011 through 14 April 2011
ER -