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

BRÁZDIL, Tomáš; Javier ESPARZA and 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, p. 521-530. ISBN 0-7695-2468-0.

Basic information

Original name

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

Name in Czech

Analýza a predikce chování náhodnostních sekvenčních programů s rekurzí

Authors

BRÁZDIL, Tomáš (203 Czech Republic); Javier ESPARZA (724 Spain) and Antonín KUČERA (276 Germany, guarantor)

Edition

Los Alamitos, California, Proceedings of the 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2005), p. 521-530, 10 pp. 2005

Publisher

IEEE Computer Society

---

Other information

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

RIV identification code

RIV/00216224:14330/05:00012708

Organization unit

Faculty of Informatics

ISBN

0-7695-2468-0

UT WoS

000234538200049

Keywords in English

Probabilistic Pushdown Automata; Infinite Markov Chains; Quantitative Analysis

Tags

Infinite Markov Chains, Probabilistic Pushdown Automata, Quantitative Analysis

---

Abstract

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.

In Czech

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.

---

Links

GA201/03/1161, research and development project	Name: Verifikace nekonečně stavových systémů Investor: Czech Science Foundation, Verification of infinite-state systems
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
1M0545, research and development project	Name: Institut Teoretické Informatiky Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science