Measuring Performance of Continuous-Time Stochastic Processes using Timed Automata

• Authors: BRÁZDIL Tomáš; KRČÁL Jan; KŘETÍNSKÝ Jan; KUČERA Antonín; ŘEHÁK Vojtěch
• Year of publication: 2011
• Type: Article in Proceedings
• Conference: HSCC 11: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control
• MU Faculty or unit: Faculty of Informatics
• Field: Informatics
• Keywords: semi-Markov processes; timed automata
• Description: 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 dened 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.

Related projects

• Institute for Theoretical Computer Science
• Highly Parallel and Distributed Computing Systems
• New possibilities in automatic verification of network protocols
• Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů
• Formální metody pro analýzu a verifikaci komplexních systémů
• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace
• Posílení zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity