Author name cluster

Vojtěch Forejt

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

1 author row

TCS Journal 2016 Journal Article

Expected reachability-time games

Vojtěch Forejt
Marta Kwiatkowska
Gethin Norman
Ashutosh Trivedi

Probabilistic timed automata are a suitable formalism to model systems with real-time, nondeterministic and probabilistic behaviour. We study two-player zero-sum games on such automata where the objective of the game is specified as the expected time to reach a target. The two players—called player Min and player Max—compete by proposing timed moves simultaneously and the move with a shorter delay is performed. The first player attempts to minimise the given objective while the second tries to maximise the objective. We observe that these games are not determined, and study decision problems related to computing the upper and lower values, showing that the problems are decidable and lie in the complexity class NEXPTIME ∩ co-NEXPTIME.

Details DOI

I&C Journal 2014 Journal Article

Language equivalence of probabilistic pushdown automata

Vojtěch Forejt
Petr Jančar
Stefan Kiefer
James Worrell

We study the language equivalence problem for probabilistic pushdown automata (pPDA) and their subclasses. We show that the problem is interreducible with the multiplicity equivalence problem for context-free grammars, the decidability of which has been open for several decades. Interreducibility also holds for pPDA with one control state. In contrast, for the case of a one-letter input alphabet we show that pPDA language equivalence (and hence multiplicity equivalence of context-free grammars) is in PSPACE and at least as hard as the polynomial identity testing problem.

Details DOI

I&C Journal 2013 Journal Article

Continuous-time stochastic games with time-bounded reachability

Tomáš Brázdil
Vojtěch Forejt
Jan Krčál
Jan Křetínský
Antonín Kučera

We study continuous-time stochastic games with time-bounded reachability objectives and time-abstract strategies. 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. Further, we show how to compute ε-optimal strategies in finite games and provide detailed complexity estimations. Moreover, we show how to compute ε-optimal strategies in infinite games with finite branching and bounded rates where the bound as well as the successors of a given state are effectively computable. Finally, we show how to compute optimal strategies in finite uniform games.

Details DOI

I&C Journal 2008 Journal Article

Reachability in recursive Markov decision processes

Tomáš Brázdil
Václav Brožek
Vojtěch Forejt
Antonín Kučera

We consider a class of infinite-state Markov decision processes generated by stateless pushdown automata. This class corresponds to 1 1 2 -player games over graphs generated by BPA systems or (equivalently) 1-exit recursive state machines. An extended reachability objective is specified by two sets S and T of safe and terminal stack configurations, where the membership to S and T depends just on the top-of-the-stack symbol. The question is whether there is a suitable strategy such that the probability of hitting a terminal configuration by a path leading only through safe configurations is equal to (or different from) a given x ∈ { 0, 1 }. We show that the qualitative extended reachability problem is decidable in polynomial time, and that the set of all configurations for which there is a winning strategy is effectively regular. More precisely, this set can be represented by a deterministic finite-state automaton with a fixed number of control states. This result is a generalization of a recent theorem by Etessami and Yannakakis which says that the qualitative termination for 1-exit RMDPs (which exactly correspond to our 1 1 2 -player BPA games) is decidable in polynomial time. Interestingly, the properties of winning strategies for the extended reachability objectives are quite different from the ones for termination, and new observations are needed to obtain the result. As an application, we derive the EXPTIME-completeness of the model-checking problem for 1 1 2 -player BPA games and qualitative PCTL formulae.

Details DOI