Measuring Performance of Continuous-Time Stochastic Processes using Timed Automata

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

Základní údaje

• Originální název: Measuring Performance of Continuous-Time Stochastic Processes using Timed Automata
• Autoři: BRÁZDIL, Tomáš (203 Česká republika, domácí), Jan KRČÁL (203 Česká republika, domácí), Jan KŘETÍNSKÝ (203 Česká republika, domácí), Antonín KUČERA (203 Česká republika, garant, domácí) a Vojtěch ŘEHÁK (203 Česká republika, domácí).
• Vydání: New York, HSCC 11: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, od s. 33-42, 10 s. 2011.
• Nakladatel: ACM

Další údaje

• Originální jazyk: angličtina
• Typ výsledku: Stať ve sborníku
• Obor: 10201 Computer sciences, information science, bioinformatics
• Stát vydavatele: Spojené státy
• Utajení: není předmětem státního či obchodního tajemství
• Forma vydání: tištěná verze "print"
• Kód RIV: RIV/00216224:14330/11:00049786
• Organizační jednotka: Fakulta informatiky
• ISBN: 978-1-4503-0629-4
• UT WoS: 000290062600005
• Klíčová slova anglicky: semi-Markov processes; timed automata
• Štítky: best3
• Příznaky: Mezinárodní význam, Recenzováno

Anotace

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.

Anotace česky

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.

Návaznosti

• GD102/09/H042, projekt VaV: Název: 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: Grantová agentura ČR, 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ů

• GP201/08/P459, projekt VaV: Název: Nové možnosti automatické verifikace síťových protokolů

Investor: Grantová agentura ČR, Nové možnosti automatické verifikace síťových protokolů

• MSM0021622419, záměr: Název: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy

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

Investor: Masarykova univerzita, Posílení zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

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

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

• P202/10/1469, interní kód MU: Název: Formální metody pro analýzu a verifikaci komplexních systémů
• 1M0545, projekt VaV: Název: Institut Teoretické Informatiky

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky