TY - GEN

T1 - On the memory consumption of probabilistic pushdown automata

AU - Brazdil, Tomaš

AU - Esparza, Javier

AU - Kiefer, Stefan

PY - 2009

Y1 - 2009

N2 - We investigate the problem of evaluating memory consumption for systems modelled by probabilistic pushdown automata (pPDA). The space needed by a run of a pPDA is the maximal height reached by the stack during the run. The problem is motivated by the investigation of depth-first computations that play an important role for space-efficient schedulings of multithreaded programs. We study the computation of both the distribution of the memory consumption and its expectation. For the distribution, we show that a naive method incurs an exponential blow-up, and that it can be avoided using linear equation systems. We also suggest a possibly even faster approximation method. Given ε > 0, these methods allow to compute bounds on the memory consumption that are exceeded with a probability of at most ε. For the expected memory consumption, we show that whether it is infinite can be decided in polynomial time for stateless pPDA (pBPA) and in polynomial space for pPDA. We also provide an iterative method for approximating the expectation. We show how to compute error bounds of our approximation method and analyze its convergence speed. We prove that our method converges linearly, i.e., the number of accurate bits of the approximation is a linear function of the number of iterations.

AB - We investigate the problem of evaluating memory consumption for systems modelled by probabilistic pushdown automata (pPDA). The space needed by a run of a pPDA is the maximal height reached by the stack during the run. The problem is motivated by the investigation of depth-first computations that play an important role for space-efficient schedulings of multithreaded programs. We study the computation of both the distribution of the memory consumption and its expectation. For the distribution, we show that a naive method incurs an exponential blow-up, and that it can be avoided using linear equation systems. We also suggest a possibly even faster approximation method. Given ε > 0, these methods allow to compute bounds on the memory consumption that are exceeded with a probability of at most ε. For the expected memory consumption, we show that whether it is infinite can be decided in polynomial time for stateless pPDA (pBPA) and in polynomial space for pPDA. We also provide an iterative method for approximating the expectation. We show how to compute error bounds of our approximation method and analyze its convergence speed. We prove that our method converges linearly, i.e., the number of accurate bits of the approximation is a linear function of the number of iterations.

UR - http://www.scopus.com/inward/record.url?scp=84880205213&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.FSTTCS.2009.2306

DO - 10.4230/LIPIcs.FSTTCS.2009.2306

M3 - Conference contribution

AN - SCOPUS:84880205213

SN - 9783939897132

T3 - Leibniz International Proceedings in Informatics, LIPIcs

SP - 49

EP - 60

BT - Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2009 - 29th Annual Conference, Proceedings

T2 - 29th International Conference on the Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2009

Y2 - 15 December 2009 through 17 December 2009

ER -