Technical Reports
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.
