BRÁZDIL, Tomáš, Javier ESPARZA a Antonín KUČERA. Analysis and Prediction of the Long-Run Behavior of Probabilistic Sequential Programs with Recursion. In Proceedings of the 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2005). Los Alamitos, California: IEEE Computer Society, 2005. s. 521-530, 10 s. ISBN 0-7695-2468-0.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Analysis and Prediction of the Long-Run Behavior of Probabilistic Sequential Programs with Recursion
Název česky Analýza a predikce chování náhodnostních sekvenčních programů s rekurzí
Autoři BRÁZDIL, Tomáš (203 Česká republika), Javier ESPARZA (724 Španělsko) a Antonín KUČERA (276 Německo, garant).
Vydání Los Alamitos, California, Proceedings of the 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2005), od s. 521-530, 10 s. 2005.
Nakladatel IEEE Computer Society
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor Computer sciences, information science, bioinformatics
Stát vydavatele Spojené státy americké
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/05:00012708
Organizační jednotka Fakulta informatiky
ISBN 0-7695-2468-0
UT WoS 000234538200049
Klíčová slova anglicky Probabilistic Pushdown Automata; Infinite Markov Chains; Quantitative Analysis
Štítky Infinite Markov Chains, Probabilistic Pushdown Automata, Quantitative Analysis
Změnil Změnil: doc. RNDr. Tomáš Brázdil, Ph.D., učo 4074. Změněno: 13. 2. 2006 12:38.
Anotace
We introduce a family of long-run average properties of Markov chains that are useful for purposes of performance and reliability analysis, and show that these properties can effectively be checked for a subclass of infinite-state Markov chains generated by probabilistic programs with recursive procedures. We also show how to predict these properties by analyzing finite prefixes of runs, and present an efficient prediction algorithm for the mentioned subclass of Markov chains.
Anotace česky
Zavedeme třídu limitních vlastností Markovových řetězců, které umožňují formulovat řadu požadavků na výkon a spolehlivost systémů, které jsou těmito řetězci popsány. Dokážeme, že tyto vlastnosti jsou algoritmicky ověřitelné pro řetězce generované náhodnostními programy s rekurzivními procedurami. Rovněž ukážeme, jak lze tyto vlastnosti předvídat na základě konečného prefixu daného běhu.
Návaznosti
GA201/03/1161, projekt VaVNázev: Verifikace nekonečně stavových systémů
Investor: Grantová agentura ČR, Standardní projekty
MSM0021622419, záměrNázev: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumné záměry
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Výzkumná centra (Národní program výzkumu)
VytisknoutZobrazeno: 21. 10. 2019 17:44