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, 10 pp. ISBN 0-7695-2468-0.
Other formats:   BibTeX LaTeX RIS
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
Original language English
Type of outcome Proceedings paper
Field of Study 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
Changed by Changed by: doc. RNDr. Tomáš Brázdil, Ph.D., učo 4074. Changed: 13/2/2006 12:38.
Abstract
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.
Abstract (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 projectName: Verifikace nekonečně stavových systémů
Investor: Czech Science Foundation, Standard Projects
MSM0021622419, plan (intention)Name: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministry of Education, Youth and Sports of the CR, Research Intents
1M0545, research and development projectName: Institut Teoretické Informatiky
Investor: Ministry of Education, Youth and Sports of the CR, Research Centres (National Research Programme)
PrintDisplayed: 17/11/2019 19:33