A List by Author: Antonín Kučera
- e-mail:
- tony(a)fi.muni.cz
- home page:
- https://www.fi.muni.cz/usr/kucera/
Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes
by
Tomáš Brázdil,
Václav Brožek,
Krishnendu Chatterjee,
Vojtěch Forejt,
Antonín Kučera,
A full version of the paper presented at conference LICS 2011. April 2011, 32 pages.
FIMU-RS-2011-02.
Available as Postscript,
PDF.
Abstract:
We study Markov decision processes (MDPs) with multiple
limit-average (or mean-payoff) functions. We consider two different
objectives, namely, expectation and satisfaction objectives. Given
an MDP with k reward functions, in the expectation objective the
goal is to maximize the expected limit-average value, and in the satisfaction
objective the goal is to maximize the probability of runs such that
the limit-average value stays above a given vector.
We show that
under the expectation objective, in contrast to the single-objective
case, both randomization and memory are necessary for strategies,
and that finite-memory randomized strategies are sufficient.
Under the satisfaction objective, in contrast to the
single-objective case, infinite memory is necessary
for strategies, and that randomized memoryless strategies
are sufficient for epsilon-approximation, for all
epsilon. We further prove that
the decision problems for both expectation and satisfaction
objectives can be solved in polynomial time and the trade-off curve
(Pareto curve) can be epsilon-approximated in time polynomial
in the size of the MDP and 1/epsilon, and exponential
in the number of reward functions, for all epsilon>0. Our
results also reveal flaws in
previous work for MDPs with multiple
mean-payoff functions under the expectation objective, correct the
flaws and obtain improved results.
Stochastic Real-Time Games with Qualitative Timed Automata Objectives
by
Tomáš Brázdil,
Jan Krčál,
Jan Křetínský,
Antonín Kučera,
Vojtěch Řehák,
A full version of the paper presented at CONCUR 2010. August 2010, 39 pages.
FIMU-RS-2010-05.
Available as Postscript,
PDF.
Abstract:
We consider two-player stochastic games over real-time probabilistic
processes where the winning objective is specified by a timed
automaton. The goal of player I is to play in such a way that the
play (a timed word) is accepted by the timed automaton with probability
one. Player II aims at the opposite. We prove that whenever
player I has a winning strategy, then she also has a strategy that
can be specified by a timed automaton. The strategy automaton reads the
history of a play, and the decisions taken by the strategy depend only on
the region of the resulting configuration. We also give an
exponential-time algorithm which computes a winning timed automaton
strategy if it exists.
Reachability Games on Extended Vector Addition Systems with States
by
Tomáš Brázdil,
Petr Jančar,
Antonín Kučera,
A full version of the paper presented at ICALP 2010. February 2010, 38 pages.
FIMU-RS-2010-02.
Available as Postscript,
PDF.
Abstract:
We consider two-player turn-based games with zero-reachability and zero-safety objectives generated by extended vector addition systems with states. Although the problem of deciding the winner in such games is undecidable in general, we identify several decidable and even tractable subcases of this problem obtained by restricting the number of counters and/or the sets of target configurations.
Continuous-Time Stochastic Games with Time-Bounded Reachability
by
Tomáš Brázdil,
Vojtěch Forejt,
Jan Krčál,
Jan Křetínský,
Antonín Kučera,
A full version of the paper presented at FST&TCS 2009. October 2009, 46 pages.
FIMU-RS-2009-09.
Available as Postscript,
PDF.
Abstract:
We study continuous-time stochastic games with
time-bounded reachability objectives. We show that each vertex in
such a game has a value (i.e., an equilibrium probability),
and we classify the conditions under which optimal strategies exist.
Finally, we show how to compute optimal strategies in finite uniform
games, and how to compute e-optimal strategies in
finitely-branching games with bounded rates (for finite games, we
provide detailed complexity estimations).
Qualitative Reachability in Stochastic BPA Games
by
Václav Brožek,
Tomáš Brázdil,
Antonín Kučera,
Jan Obdržálek,
A full version of the paper presented at STACS 2009. May 2009, 37 pages.
FIMU-RS-2009-01.
Available as Postscript,
PDF.
Abstract:
We consider a class of infinite-state stochastic games generated by stateless pushdown
automata (or, equivalently, 1-exit recursive state machines), where the winning
objective is specified by a regular set of target configurations and a qualitative
probability constraint ‘>0’ or ‘=1’. The goal of one player is to maximize the probability
of reaching the target set so that the constraint is satisfied, while the other
player aims at the opposite. We show that the winner in such games can be determined
in NP intersection co-NP. Further, we prove that the winning regions for both players
are regular, and we design algorithms which compute the associated finite-state automata.
Finally, we show that winning strategies can be synthesized effectively.
Discounted Properties of Probabilistic Pushdown Automata
by
Tomáš Brázdil,
Václav Brožek,
Jan Holeček,
Antonín Kučera,
A full version of the paper presented at LPAR 2008 September 2008, 31 pages.
FIMU-RS-2008-08.
Available as Postscript,
PDF.
Abstract:
We show that several basic discounted properties of probabilistic
pushdown automata related both to terminating and non-terminating runs
can be efficiently approximated up to an arbitrarily
small given precision.
Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives
by
Tomáš Brázdil,
Vojtěch Forejt,
Antonín Kučera,
A full version of the paper presented at ICALP 2008. December 2008, 48 pages.
FIMU-RS-2008-05.
Available as Postscript,
PDF.
Abstract:
We show that controller synthesis and verification problems for
Markov decision processes with qualitative PECTL* objectives
are 2-EXPTIME complete. More precisely, the algorithms are
polynomial in the size of a given Markov decision process
and doubly exponential in the size of a given qualitative PECTL*
formula. Moreover, we show that if a given qualitative PECTL*
objective is achievable by some strategy, then it is also
achievable by an effectively constructible one-counter
strategy, where the associated complexity bounds are essentially
the same as above. For the fragment of qualitative PCTL objectives,
we obtain EXPTIME completeness and the algorithms are only singly
exponential in the size of the formula.
The Satisfiability Problem for Probabilistic CTL
by
Tomáš Brázdil,
Vojtěch Forejt,
Jan Křetínský,
Antonín Kučera,
A full version of the paper presented at LICS 2008. June 2008, 34 pages.
FIMU-RS-2008-03.
Available as Postscript,
PDF.
Abstract:
We study the satisfiability problem for qualitative PCTL
(Probabilistic Computation Tree Logic), which is obtained from
"ordinary" CTL by replacing the EX, AX, EU, and AU operators
with their qualitative
counterparts X>0, X=1, U>0, and U=1, respectively.
As opposed to CTL, qualitative PCTL does not have a small model
property, and there are even qualitative PCTL formulae which have only
infinite-state models. Nevertheless, we show that the satisfiability problem
for qualitative PCTL is EXPTIME-complete and we give an
exponential-time algorithm which for a given formula
computes a finite description of a model (if it exists),
or answers "not satisfiable" (otherwise). We also consider the
finite satisfiability problem and provide analogous results. That is,
we show that the finite satisfiability problem for qualitative PCTL
is EXPTIME-complete, and every finite satisfiable formula has a model
of an exponential size which can effectively be constructed in
exponential time.
Finally, we give some results about the quantitative PCTL, where
the numerical bounds in probability constraints can be arbitrary rationals
between 0 and 1. We prove that the problem whether a given quantitative
PCTL formula has a model of the branching degree at most k, where k > 1 is an arbitrary but fixed constant, is highly undecidable.
We also show that every satisfiable formula F has a model with
branching degree at most |F| + 2. However, this does not yet
imply the undecidability of the satisfiability problem for
quantitative PCTL, and we in fact conjecture the opposite.
Stochastic Games with Branching-Time Winning Objectives
by
Tomáš Brázdil,
Václav Brožek,
Vojtěch Forejt,
Antonín Kučera,
A full version of the paper presented at LICS 2006. September 2006, 37 pages.
FIMU-RS-2006-02.
Available as Postscript,
PDF.
Abstract:
We consider stochastic turn-based games where the
winning objectives are given by formulae of the branching-time
logic PCTL. These games are generally not determined and
winning strategies may require memory and/or randomization.
Our main results concern history-dependent strategies.
In particular, we show that the problem whether there
exists a history-dependent winning strategy
in 1.5-player games is highly undecidable, even
for objectives formulated in the
L(F^{=5/8},F^{=1},F^{>0},G^{=1}) fragment of
PCTL. On the other hand, we show that the problem becomes decidable
(and in fact EXPTIME-complete) for the
L(F^{=1},F^{>0},G^{=1}) fragment of PCTL, where winning
strategies require only finite memory. This result is tight in the
sense that winning strategies for
L(F^{=1},F^{>0},G^{=1},G^{>0}) objectives may
already require infinite memory.
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.
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.
Characteristic Patterns for LTL
by
Antonín Kučera,
Jan Strejček,
A full version of the paper presented at Sofsem 2005. December 2004, 22 pages.
FIMU-RS-2004-10.
Available as Postscript,
PDF.
Abstract:
We give a new characterization of those languages that are definable
in fragments of LTL where the nesting depths of X and
U modalities are bounded by given constants. This brings further results
about various LTL fragments. We also propose a generic method for
decomposing LTL formulae into an equivalent disjunction of ``semantically
refined" LTL formulae, and indicate how this result can be used to
improve the functionality of existing LTL model-checkers.
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.
A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications
by
Antonín Kučera,
Philippe Schnoebelen,
A full version of the paper presented at CONCUR`04. June 2004, 32 pages.
FIMU-RS-2004-05.
Available as Postscript,
PDF.
Abstract:
We introduce a generic family of behavioral relations for which the
problem of comparing an arbitrary transition system to some
finite-state specification can be reduced to a model checking problem
against simple modal formulae. As an application, we derive
decidability of several regular equivalence problems for well-known
families of infinite-state systems.
An Effective Characterization of Properties Definable by LTL Formulae with a Bounded Nesting Depth of the Next-Time Operator
by
Antonín Kučera,
Jan Strejček,
May 2004, 11 pages.
FIMU-RS-2004-04.
Available as Postscript,
PDF.
Abstract:
It is known that an LTL property is expressible by an LTL formula
without any next-time operator if and only if the property is
stutter invariant. It is also known that the problem whether a
given LTL property is stutter invariant is PSPACE-complete. We
extend these results to fragments of LTL obtained by restricting the
nesting depth of the next-time operator to a given n.
Some interesting facts about the logic LTL follow as simple
corollaries.
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.
The Stuttering Principle Revisited: On the Expressiveness of Nested X and U Operators in the Logic LTL
by
Antonín Kučera,
Jan Strejček,
A full version of the paper presented at CSL`02. July 2002, 24 pages.
FIMU-RS-2002-03.
Available as Postscript,
PDF.
Abstract:
It is known that LTL formulae without the `next` operator
are invariant under the so-called
stutter-equivalence of
words. In this paper we extend this principle to general
LTL formulae with given nesting depths of the `next` and `until` operators. This allows us to prove the semantical strictness of three
natural hierarchies of LTL formulae, which are
parametrized either
by the nesting depth of just one of the two operators,
or by both of them. As another interesting corollary
we obtain an alternative
characterization of LTL languages, which are exactly the
regular languages closed under the generalized form of stutter equivalence. We also indicate how to tackle the state-space explosion problem with the help of presented results.
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.
On Simulation-Checking with Sequential Systems
by
Antonín Kučera,
This is a full version of the paper accepted for ASIAN 2000. September 2000, 34 pages.
FIMU-RS-2000-05.
Available as Postscript,
PDF.
Abstract:
We present new complexity results for simulation-checking and model-checking with infinite-state systems generated by pushdown automata and their proper subclasses of one-counter automata and one-counter nets (one-counter nets are "weak" one-counter automata computationally equivalent to Petri nets with at most one unbounded place).
As for simulation-checking, we show the following: a) simulation equivalence between pushdown processes and finite-state processes is EXPTIME-complete; b) simulation equivalence between processes of one-counter automata and finite-state processes is coNP-hard; c) simulation equivalence between processes of one-counter nets and finite-state processes is in P (to the best of our knowledge, it is the first (and rather tight) polynomiality result for simulation with infinite-state processes).
As for model-checking, we prove that a) the problem of simulation-checking between processes of pushdown automata (or one-counter automata, or one-counter nets) and finite-state processes are polynomially reducible to the model-checking problem with a fixed formula F = nu X. [z]<z> X of the modal mu-calculus. Consequently, model-checking with F is EXPTIME-complete for pushdown processes and coNP-hard for processes of one-counter automata; b) model-checking with a fixed formula <>[a]<>[b]ff of the logic EF (a simple fragment of CTL) is NP-hard for processes of OC nets, and model-checking with another fixed formula []<a>[]<b>tt of EF is coNP-hard. Consequently, model-checking with any temporal logic which can express these simple formulae is computationally hard even for the (very simple) sequential processes of OC-nets.
Efficient Verification Algorithms for One-Counter Processes
by
Antonín Kučera,
This is a full version of the paper presented at ICALP 2000. March 2000, 24 pages.
FIMU-RS-2000-03.
Available as Postscript,
PDF.
Abstract:
We study the problem of strong/weak bisimilarity between processes of one-counter automata and finite-state processes. We show that the problem of weak bisimilarity between processes of one-counter nets (which are "weak" one-counter automata) and finite-state processes is DP-hard (in particular, it means that the problem is both NP and co-NP hard). The same technique is used to demonstrate co-NP hardness of strong bisimilarity between processes of one-counter nets. Then we design an algorithm which decides weak bisimilarity between processes of one-counter automata and finite-state processes in time which is polynomial for most "practical" instances, giving a characterization of all hard instances as a byproduct. Moreover, we show how to efficiently compute a rather tight bound for the time which is needed to solve a given instance. Finally, we prove that the problem of strong bisimilarity between processes of one-counter automata and finite-state processes is in P.
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.
Bisimilarity of Processes with Finite-state Systems
by
Petr Jančar,
Antonín Kučera,
These results will be presented at INFINITY`97 workshop. May 1997, 19 pages.
FIMU-RS-97-02.
Available as Postscript,
PDF.
Abstract:
We describe a general method for deciding bisimilarity for pairs of processes where one process has finitely many states. We apply this method to pushdown processes and to PA processes. We also demonstrate that the mentioned problem is undecidable for `state-extended` PA processes.
How to Parallelize Sequential Processes
by
Antonín Kučera,
Accepted to the 8th International Conference on Concurrency Theory (CONCUR`97). December 1996, 24 pages.
FIMU-RS-96-05.
Available as Postscript,
PDF.
Abstract:
A process is prime if it cannot be decomposed into a parallel product of nontrivial processes. We characterize all non-prime normed BPA processes together with their decompositions in terms of normal forms which are designed in this paper. Then we show that it is decidable whether a given normed BPA process is prime and if not, its decomposition can be effectively constructed. This brings other positive decidability results. Finally, we prove that bisimilarity is decidable in a large subclass of normed PA processes.
Comparing Expressibility of Normed BPA and Normed BPP Processes
by
Ivana Černá,
Mojmír Křetínský,
Antonín Kučera,
This is a full version of the paper which is to be presented at CSL`96. June 1996, 28 pages.
FIMU-RS-96-02.
Available as Postscript,
PDF.
Abstract:
We compare the classes of behaviours (transition systems) which can be generated by normed BPA_{\tau} and normed BPP_{\tau} processes. We exactly classify the intersection of these two classes, i.e., the class of transition systems which can be equivalently (up to bisimilarity) described by the syntax of normed BPA_{\tau} and normed BPP_{\tau} processes. We provide such a characterisation for classes of normed BPA and normed BPP processes as well.
Next we show that it is decidable in polynomial time whether for a given normed BPA_{\tau} (or BPP_{\tau} respectively) process X there is some (unspecified) normed BPP_{\tau} (or BPA_{\tau} respectively) process X` such that X is bisimilar to X`. Moreover, if the answer is positive then our algorithms also construct the process X`. Simplified versions of the algorithms mentioned above for normed BPA and normed BPP are given too.
As an immediate (but important) consequence we also obtain the decidability of bisimilarity in the union of normed BPA_{\tau} and normed BPP_{\tau} processes.
Regularity is Decidable for Normed PA Processes in Polynomial Time
by
Antonín Kučera,
This paper is going to be presented at FST&TCS`96 conference, LNCS 1180, Springer-Verlag. February 1996, 17 pages.
FIMU-RS-96-01.
Available as Postscript,
PDF.
Abstract:
A process X is regular if it is bisimilar to a process X` with finitely many states. We prove that regularity of normed PA processes is decidable and we present a practically usable polynomial-time algorithm. Moreover, if the tested normed PA process X is regular then the process X` can be effectively constructed. It implies decidability of bisimulation equivalence for any pair of processes such that one process is a normed PA process and the other process has finitely many states.