Author name cluster

Jan Křetínský

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.

8 papers

1 author row

I&C Journal 2022 Journal Article

Comparison of algorithms for simple stochastic games

Jan Křetínský
Emanuel Ramneantu
Alexander Slivinskiy
Maximilian Weininger

Simple stochastic games are turn-based 2½-player zero-sum graph games with a reachability objective. The problem is to compute the winning probabilities as well as the optimal strategies of both players. In this paper, we compare the three known classes of algorithms – value iteration, strategy iteration and quadratic programming – both theoretically and practically. Further, we suggest several improvements for all algorithms, including the first approach based on quadratic programming that avoids transforming the stochastic game to a stopping one. Our extensive experiments show that these improvements can lead to significant speed-ups. We implemented all algorithms in PRISM-games 3. 0, thereby providing the first implementation of quadratic programming for solving simple stochastic games.

Details DOI

I&C Journal 2022 Journal Article

Value iteration for simple stochastic games: Stopping criterion and learning algorithm

Julia Eisentraut
Edon Kelmendi
Jan Křetínský
Maximilian Weininger

The classical problem of reachability in simple stochastic games is typically solved by value iteration (VI), which produces a sequence of under-approximations of the value of the game, but is only guaranteed to converge in the limit. We provide an additional converging sequence of over-approximations, based on an analysis of the game graph. Together, these two sequences entail the first error bound and hence the first stopping criterion for VI on simple stochastic games, indicating when the algorithm can be stopped for a given precision. Consequently, VI becomes an anytime algorithm returning the approximation of the value and the current error bound. We further use this error bound to provide a learning-based asynchronous VI algorithm; it uses simulations and thus often avoids exploring the whole game graph, but still yields the same guarantees. Finally, we experimentally show that the overhead for computing the additional sequence of over-approximations often is negligible.

Details DOI

IJCAI Conference 2021 Conference Paper

LTL-Constrained Steady-State Policy Synthesis

Jan Křetínský

Decision-making policies for agents are often synthesized with the constraint that a formal specification of behaviour is satisfied. Here we focus on infinite-horizon properties. On the one hand, Linear Temporal Logic (LTL) is a popular example of a formalism for qualitative specifications. On the other hand, Steady-State Policy Synthesis (SSPS) has recently received considerable attention as it provides a more quantitative and more behavioural perspective on specifications, in terms of the frequency with which states are visited. Finally, rewards provide a classic framework for quantitative properties. In this paper, we study Markov decision processes (MDP) with the specification combining all these three types. The derived policy maximizes the reward among all policies ensuring the LTL specification with the given probability and adhering to the steady-state constraints. To this end, we provide a unified solution reducing the multi-type specification to a multi-dimensional long-run average reward. This is enabled by Limit-Deterministic Büchi Automata (LDBA), recently studied in the context of LTL model checking on MDP, and allows for an elegant solution through a simple linear programme. The algorithm also extends to the general omega-regular properties and runs in time polynomial in the sizes of the MDP as well as the LDBA.

PDF Details DOI

GandALF Workshop 2020 Workshop Paper

Comparison of Algorithms for Simple Stochastic Games

Jan Křetínský
Emanuel Ramneantu
Alexander Slivinskiy
Maximilian Weininger

Simple stochastic games are turn-based 2. 5-player zero-sum graph games with a reachability objective. The problem is to compute the winning probability as well as the optimal strategies of both players. In this paper, we compare the three known classes of algorithms – value iteration, strategy iteration and quadratic programming – both theoretically and practically. Further, we suggest several improvements for all algorithms, including the first approach based on quadratic programming that avoids transforming the stochastic game to a stopping one. Our extensive experiments show that these improvements can lead to significant speed-ups. We implemented all algorithms in PRISM-games 3. 0, thereby providing the first implementation of quadratic programming for solving simple stochastic games.

PDF Details DOI

I&C Journal 2020 Journal Article

Logical vs. behavioural specifications

Nikola Beneš
Uli Fahrenberg
Jan Křetínský
Axel Legay
Louis-Marie Traonouez

There are two fundamentally different approaches for specifying and verifying properties of systems. The logical approach makes use of specifications given as formulae of temporal or modal logics and relies on efficient model checking algorithms; the behavioural approach exploits various equivalence or refinement checking methods, provided the specifications are given in the same formalism as implementations. In this paper we provide translations between the logical formalism of ν-calculus and the behavioural formalism of disjunctive modal transition systems. The translations preserve structural properties of the input specification and allow us to perform logical operations on the behavioural specifications as well as behavioural compositions on logical formulae. The unification of both approaches provides additional methods for component-based stepwise design.

Details DOI

Highlights Conference 2018 Conference Abstract

A Journey from LTL to Your Favourite Automaton

Jan Křetínský

ABSTRACT. The automata-theoretic approach to LTL model checking relies on translations of LTL formulae into automata. Efficiency of and techniques used in these translations differ depending on the target automata class. For instance, deterministic automata were traditionally produced using Safra's construction, which is quite complex and practically not very efficient. In this work, we present a unified translation of LTL formulas into deterministic Rabin automata, limit-deterministic Büchi automata, and nondeterministic Büchi automata. The translations yield automata of asymptotically optimal size (double or single exponential, respectively). All three translations are derived from one single Master Theorem of purely logical nature. The Master Theorem decomposes the language of a formula into a positive boolean combination of languages that can be translated into automata by elementary means. In particular, Safra's, ranking, and breakpoint constructions used in other translations are not needed.

Details

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 2012 Journal Article

EXPTIME-completeness of thorough refinement on modal transition systems

Nikola Beneš
Jan Křetínský
Kim G. Larsen
Jiří Srba

Modal transition systems (MTS), a specification formalism introduced more than 20 years ago, has recently received a considerable attention in several different areas. Many of the fundamental questions related to MTSs have already been answered. However, the problem of the exact computational complexity of thorough refinement checking between two finite MTSs remained unsolved. We settle down this question by showing EXPTIME-completeness of thorough refinement checking on finite MTSs. The upper-bound result relies on a novel algorithm running in single exponential time providing a direct goal-oriented way to decide thorough refinement. If the right-hand side MTS is moreover deterministic, or has a fixed size, the running time of the algorithm becomes polynomial. The lower-bound proof is achieved by reduction from the acceptance problem of alternating linear bounded automata and the problem remains EXPTIME-hard even if the left-hand side MTS is fixed and deterministic.

Details DOI