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

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BRÁZDIL Tomáš ESPARZA Javier KUČERA Antonín

Year of publication 2005
Type Article in Proceedings
Conference Proceedings of the 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2005)
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords Probabilistic Pushdown Automata; Infinite Markov Chains; Quantitative Analysis
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.