On the Memory Consumption of Probabilistic Pushdown Automata

Authors Tomas Brazdil, Javier Esparza, Stefan Kiefer



PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2009.2306.pdf
  • Filesize: 125 kB
  • 12 pages

Document Identifiers

Author Details

Tomas Brazdil
Javier Esparza
Stefan Kiefer

Cite As Get BibTex

Tomas Brazdil, Javier Esparza, and Stefan Kiefer. On the Memory Consumption of Probabilistic Pushdown Automata. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 49-60, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009) https://doi.org/10.4230/LIPIcs.FSTTCS.2009.2306

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.

Subject Classification

Keywords
  • Pushdown automata
  • probabilistic systems
  • verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail