Measuring Performance of Continuous-Time Stochastic Processes using Timed Automata

BRÁZDIL, Tomáš, Jan KRČÁL, Jan KŘETÍNSKÝ, Antonín KUČERA and Vojtěch ŘEHÁK. Measuring Performance of Continuous-Time Stochastic Processes using Timed Automata. Online. In Emilio Frazzoli, Radu Grosu. HSCC 11: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control. New York: ACM, 2011. p. 33-42. ISBN 978-1-4503-0629-4. [citováno 2024-04-23]

Basic information

• Original name: Measuring Performance of Continuous-Time Stochastic Processes using Timed Automata
• Authors: BRÁZDIL, Tomáš (203 Czech Republic, belonging to the institution), Jan KRČÁL (203 Czech Republic, belonging to the institution), Jan KŘETÍNSKÝ (203 Czech Republic, belonging to the institution), Antonín KUČERA (203 Czech Republic, guarantor, belonging to the institution) and Vojtěch ŘEHÁK (203 Czech Republic, belonging to the institution)
• Edition: New York, HSCC 11: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, p. 33-42, 10 pp. 2011.
• Publisher: ACM

Other information

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: United States of America
• Confidentiality degree: is not subject to a state or trade secret
• Publication form: printed version "print"
• RIV identification code: RIV/00216224:14330/11:00049786
• Organization unit: Faculty of Informatics
• ISBN: 978-1-4503-0629-4
• UT WoS: 000290062600005
• Keywords in English: semi-Markov processes; timed automata
• Tags: best3
• Tags: International impact, Reviewed

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 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.

Abstract (in Czech)

V článku jsou studovány deterministické časové automaty (DTA) jako modelově nezávislý jazyk pro specifikaci různých vlastností souvisejících s výkonem a spolehlivostí stochastických procesů se spojitým časem. Technicky jsou tyto vlastnosti definovány jako limity frekvencí výskytů lokací daného DTA, který sleduje výpočet daného stochastického procesu. Ukážeme, že uvedené vlastnosti jsou dobře definované a podáme algoritmus, který dokáže příslušné kvantitativní charakteristiky aproximovat s libovolně malou kladnou chybou.

Links

• GD102/09/H042, research and development project: Name: 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ů

Investor: Czech Science Foundation

• GP201/08/P459, research and development project: Name: Nové možnosti automatické verifikace síťových protokolů

Investor: Czech Science Foundation, New possibilities in automatic verification of network protocols

• MSM0021622419, plan (intention): Name: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems

• MUNI/A/0057/2011, interní kód MU: Name: Posílení zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKONF)

Investor: Masaryk University, Category A

• MUNI/A/0914/2009, interní kód MU: Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace (Acronym: SV-FI MAV)

Investor: Masaryk University, Category A

• P202/10/1469, interní kód MU: Name: Formální metody pro analýzu a verifikaci komplexních systémů
• 1M0545, research and development project: Name: Institut Teoretické Informatiky

Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science