License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2009.2306
URN: urn:nbn:de:0030-drops-23067
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2009/2306/
Go to the corresponding LIPIcs Volume Portal

Brazdil, Tomas ; Esparza, Javier ; Kiefer, Stefan

On the Memory Consumption of Probabilistic Pushdown Automata

pdf-format:
09005.BrazdilTomas.2306.pdf (0.1 MB)

Abstract

We investigate the problem of evaluating memory consumption for systems modelled by probabilistic pushdown automata (pPDA). The space needed by a runof a pPDA is the maximal height reached by the stack during the run. Theproblem is motivated by the investigation of depth-first computations that playan 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 anexponential blow-up, and that it can be avoided using linear equation systems.We also suggest a possibly even faster approximation method.Given~$\varepsilon>0$, these methods allow to compute bounds on the memoryconsumption that are exceeded with a probability of at most~$\varepsilon$.
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 theexpectation. We show how to compute error bounds of our approximation methodand analyze its convergence speed. We prove that our method convergeslinearly, i.e., the number of accurate bits of the approximation is a linear function of the number of iterations.

BibTeX - Entry

@InProceedings{brazdil_et_al:LIPIcs:2009:2306,
  author =	{Tomas Brazdil and Javier Esparza and Stefan Kiefer},
  title =	{{On the Memory Consumption of Probabilistic Pushdown Automata}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{49--60},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-13-2},
  ISSN =	{1868-8969},
  year =	{2009},
  volume =	{4},
  editor =	{Ravi Kannan and K. Narayan Kumar},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2009/2306},
  URN =		{urn:nbn:de:0030-drops-23067},
  doi =		{10.4230/LIPIcs.FSTTCS.2009.2306},
  annote =	{Keywords: Pushdown automata, probabilistic systems, verification}
}

Keywords: Pushdown automata, probabilistic systems, verification
Collection: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
Issue Date: 2009
Date of publication: 14.12.2009

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI