Technical Reports
A List by Author: Jan Krčál
- e-mail:
- krcal(a)fi.muni.cz
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.
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).