Analysis and Prediction of the Long-Run Behavior of Probabilistic Sequential Programs with Recursion

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. ISBN 0-7695-2468-0.

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

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í

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

---

Anotace

V originále

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.

Č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 VaV	Název: Verifikace nekonečně stavových systémů Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů
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
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky