## 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.