Technical Reports
A List by Author: Vojtěch Forejt
- e-mail:
- xforejt(a)fi.muni.cz
- home page:
- https://www.fi.muni.cz/~xforejt/
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.
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).
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.
Strategy Synthesis for Markov Decision Processes and Branching-Time Logics
by
Tomáš Brázdil,
Vojtěch Forejt,
A full version of the paper presented at CONCUR 2007 July 2007, 28 pages.
FIMU-RS-2007-03.
Available as Postscript,
PDF.
Abstract:
We consider a class of finite
$1\frac{1}{2}$-player games (Markov decision processes) where the
winning objectives are specified in
the branching-time temporal logic qPECTL$^*$
(an extension of the qualitative PCTL$^*$).
We study decidability and complexity of existence of a
winning strategy in these games.
%The logic is more expressive than the qualitative fragment of PCTL$^*$.
We identify a fragment of qPECTL$^*$ called detPECTL$^*$ for which the
existence of a winning strategy is decidable in exponential time, and
also the winning strategy can be computed in exponential time (if it exists).
Consequently we show that every formula of qPECTL$^*$ can be translated
to a formula of detPECTL$^*$ (in exponential time) so that the resulting formula
is equivalent to the original one
over finite Markov chains. From this we obtain that for the whole qPECTL$^*$,
the existence of a winning finite-memory strategy is decidable in
double exponential time. An immediate
consequence is that the existence of a
winning finite-memory strategy is decidable for the qualitative fragment of
PCTL$^*$ in triple exponential time.
We also obtain a single exponential upper bound on the same problem for
the qualitative PCTL.
Finally, we study the power of finite-memory strategies with
respect to objectives described in the qualitative PCTL.
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.