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

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

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

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

Responsible contact: unixfimunicz