A List by Author: Richard Mayr

e-mail:

mayrri(a)informatik.uni-freiburg.de

home page:

http://tele.informatik.uni-freiburg.de/~mayrri/

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 Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata

by Antonín Kučera, Richard Mayr, A full version of the paper presented at IFIP TCS 2004. April 2004, 38 pages.

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

Abstract:

We propose a generic method for deciding semantic equivalences between pushdown automata and finite-state automata. The abstract part of the method is applicable to every process equivalence which is a right PDA congruence. Practical usability of the method is demonstrated on selected equivalences which are conceptual representatives of the whole spectrum. In particular, special attention is devoted to bisimulation-like equivalences (including weak, early, delay, branching, and probabilistic bisimilarity), and it is also shown how the method applies to simulation-like and trace-like equivalences. The generality does not lead to the loss of efficiency; the algorithms obtained by applying our method are essentially time-optimal and sometimes even polynomial. The list of particular results obtained by our method includes items which are first of their kind.

Pre-Proceedings of INFINITY 2002

by Antonín Kučera, Richard Mayr, August 2002, 153 pages.

FIMU-RS-2002-04. Available as Postscript, PDF.

Abstract:

This volume contains pre-proceedings of 4th International Workshop on Verification of Infinite-State Systems (INFINITY 2002), held on August 24, 2002, in Brno, Czech Republic. The workshop was organized as a satellite event of CONCUR 2002.

Why is Simulation Harder Than Bisimulation?

by Antonín Kučera, Richard Mayr, A full version of the paper presented at CONCUR`02 June 2002, 26 pages.

FIMU-RS-2002-02. Available as Postscript, PDF.

Abstract:

Why is deciding simulation preorder (and simulation equivalence) computationally harder than deciding bisimulation equivalence on almost all known classes of processes? We try to answer this question by describing two general methods that can be used to construct direct one-to-one polynomial-time reductions from bisimulation equivalence to simulation preorder (and simulation equivalence). These methods can be applied to many classes of finitely generated transition systems, provided that they satisfy certain abstractly formulated conditions. Roughly speaking, our first method works for all classes of systems that can test for `non-enabledness` of actions, while our second method works for all classes of systems that are closed under synchronization.

On the Complexity of Semantic Equivalences for Pushdown Automata and BPA

by Antonín Kučera, Richard Mayr, A full version of the paper presented at MFCS`02. May 2002, 32 pages.

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

Abstract:

We study the complexity of comparing pushdown automata (PDA) and context-free processes (BPA) to finite-state systems, w.r.t. strong and weak simulation preorder/equivalence and strong and weak bisimulation equivalence. We present a complete picture of the complexity of all these problems. In particular, we show that strong and weak simulation preorder (and hence simulation equivalence) is EXPTIME-complete between PDA/BPA and finite-state systems in both directions. For PDA the lower bound even holds if the finite-state system is fixed, while simulation-checking between BPA and any fixed finite-state system is already polynomial. Furthermore, we show that weak (and strong) bisimilarity between PDA and finite-state systems is PSPACE-complete, while strong (and weak) bisimilarity between two (normed) PDAs is EXPTIME-hard.