D 2011

Measuring Performance of Continuous-Time Stochastic Processes using Timed Automata

BRÁZDIL, Tomáš, Jan KRČÁL, Jan KŘETÍNSKÝ, Antonín KUČERA, Vojtěch ŘEHÁK et. al.

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

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

United States of America

Confidentiality degree

není předmětem státního či obchodního tajemství

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

Tags

International impact, Reviewed

Abstract

ORIG CZ

V originále

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.

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