Technical Reports

A List by Author: Javier Esparza

e-mail:

esparza(a)informatik.uni-stuttgart.de

home page:

http://www.fmi.uni-stuttgart.de/szs/people/esparza/

On the Memory Consumption of Probabilistic Pushdown Automata

by Tomá¹ Brázdil, Javier Esparza, Stefan Kiefer, A full version of the paper presented at FSTTCS 2009 October 2009, 52 pages.

FIMU-RS-2009-07. Available as Postscript, PDF.

Abstract:

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 epsilon>0, these methods allow to compute bounds on the memory consumption that are exceeded with a probability of at most epsilon. 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.

Quantitative Analysis of Probabilistic Pushdown Automata: Expectations and Variances

by Javier Esparza, Antonín Kuèera, Richard Mayr, A full version of the paper presented at LICS 2005. July 2005, 26 pages.

FIMU-RS-2005-07. Available as Postscript, PDF.

Abstract:

Probabilistic pushdown automata (pPDA) have been identified as a natural model for probabilistic programs with recursive procedure calls. Previous works considered the decidability and complexity of the model-checking problem for pPDA and various probabilistic temporal logics. In this paper we concentrate on computing the expected values and variances of various random variables defined over runs of a given probabilistic pushdown automaton. In particular, we show how to compute the expected accumulated reward and the expected gain for certain classes of reward functions. Using these results, we show how to analyze various quantitative properties of pPDA that are not expressible in conventional probabilistic temporal logics.

Model Checking Probabilistic Pushdown Automata

by Javier Esparza, Antonín Kuèera, Richard Mayr, A full version of the paper presented at LICS`04. July 2004, 34 pages.

FIMU-RS-2004-03. Available as Postscript, PDF.

Abstract:

We consider the model checking problem for probabilistic pushdown automata (pPDA) and properties expressible in various probabilistic logics. We start with properties that can be formulated as instances of a generalized random walk problem. We prove that both qualitative and quantitative model checking for this class of properties and pPDA is decidable. Then we show that model checking for the qualitative fragment of the logic PCTL and pPDA is also decidable. Moreover, we develop an error-tolerant model checking algorithm for general PCTL and the subclass of stateless pPDA. Finally, we consider the class of properties definable by deterministic Buchi automata, and show that both qualitative and quantitative model checking for pPDA is decidable.

A Logical Viewpoint on Process-Algebraic Quotients

by Antonín Kuèera, Javier Esparza, This is a full and revised version of a paper which previously appeared in Proceedings of CSL`99. January 2000, 26 pages.

FIMU-RS-2000-01. Available as Postscript, PDF.

Abstract:

We study the following problem: Given a transition system T and its quotient T/~ under an equivalence ~, which are the sets L, L` of Hennessy-Milner formulae such that: if f belongs to L and T satisfies f, then T/~ satisfies f; if f belongs to L` and T/~ satisfies f, then T satisfies f.