A List by Author: Oldřich Stražovský
- e-mail:
- strazovsky(a)fi.muni.cz
On the Decidability of Temporal Properties of Probabilistic Pushdown Automata
by
Tomáš Brázdil,
Antonín Kučera,
Oldřich Stražovský,
A full version of the paper presented at STACS 2005. February 2005, 33 pages.
FIMU-RS-2005-01.
Available as Postscript,
PDF.
Abstract:
We consider qualitative and quantitative model-checking problems
for probabilistic pushdown automata (pPDA) and various temporal logics.
We prove that the qualitative and quantitative model-checking problem
for omega-regular properties and pPDA is in 2-EXPSPACE and
3-EXPTIME, respectively.
We also prove that model-checking the qualitative fragment of the logic
PECTL* for pPDA is in 2-EXPSPACE, and model-checking the qualitative
fragment of PCTL for pPDA is in EXPSPACE. Furthermore,
model-checking the qualitative
fragment of PCTL is shown to be EXPTIME-hard even for stateless pPDA.
Finally, we show that PCTL model-checking is undecidable for pPDA,
and PCTL+ model-checking is undecidable even for stateless pPDA.
Deciding Probabilistic Bisimilarity over Infinite-State Probabilistic Systems
by
Tomáš Brázdil,
Antonín Kučera,
Oldřich Stražovský,
A full version of the paper presented at CONCUR`04. September 2004, 26 pages.
FIMU-RS-2004-06.
Available as Postscript,
PDF.
Abstract:
We prove that probabilistic bisimilarity is decidable over
probabilistic extensions of BPA and BPP processes.
For normed subclasses of probabilistic BPA and BPP processes
we obtain polynomial-time algorithms. Further, we show
that probabilistic bisimilarity between probabilistic pushdown automata and finite-state systems is decidable in exponential time. If the number of control states in PDA
is bounded by a fixed constant,
then the algorithm needs only polynomial time.