Arrow Research search

Author name cluster

Jan Kretinsky

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.

7 papers
1 author row

Possible papers

7

NeurIPS Conference 2025 Conference Paper

Explainably Safe Reinforcement Learning

  • Sabine Rieder
  • Stefan Pranger
  • Debraj Chakraborty
  • Jan Kretinsky
  • Bettina Könighofer

Trust in a decision-making system requires both safety guarantees and the ability to interpret and understand its behavior. This is particularly important for learned systems, whose decision-making processes are often highly opaque. Shielding is a prominent model-based technique for enforcing safety in reinforcement learning. However, because shields are automatically synthesized using rigorous formal methods, their decisions are often similarly difficult for humans to interpret. Recently, decision trees became customary to represent controllers and policies. However, since shields are inherently non-deterministic, their decision tree representations become too large to be explainable in practice. To address this challenge, we propose a novel approach for explainable safe RL that enhances trust by providing human-interpretable explanations of the shield's decisions. Our method represents the shielding policy as a hierarchy of decision trees, offering top-down, case-based explanations. At design time, we use a world model to analyze the safety risks of executing actions in given states. Based on this risk analysis, we construct both the shield and a high-level decision tree that classifies states into risk categories (safe, critical, dangerous, unsafe), providing an initial explanation of why a given situation may be safety-critical. At runtime, we generate localized decision trees that explain which actions are allowed and why others are deemed unsafe. Altogether, our method facilitates the explainability of the safety aspect in the safe-by-shielding reinforcement learning. Our framework requires no additional information beyond what is already used for shielding, incurs minimal overhead, and can be readily integrated into existing shielded RL pipelines. In our experiments, we compute explanations using decision trees that are several orders of magnitude smaller than the original shield.

GandALF Workshop 2025 Workshop Paper

Sound Value Iteration for Simple Stochastic Games

  • Muqsit Azeem
  • Jan Kretinsky
  • Maximilian Weininger

Algorithmic analysis of Markov decision processes (MDP) and stochastic games (SG) in practice relies on value-iteration (VI) algorithms. Since basic VI does not provide guarantees on the precision of the result, variants of VI have been proposed that offer such guarantees. In particular, sound value iteration (SVI) not only provides precise lower and upper bounds on the result, but also converges faster in the presence of probabilistic cycles. Unfortunately, it is neither applicable to SG, nor to MDP with end components. In this paper, we extend SVI and cover both cases. The technical challenge consists mainly in proper treatment of end components, which require different handling than in the literature. Moreover, we provide several optimizations of SVI. Finally, we evaluate our prototype implementation experimentally to demonstrate its potential on systems with probabilistic cycles.

Highlights Conference 2022 Conference Abstract

LTL-Constrained Steady-State Policy Synthesis

  • Jan Kretinsky

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. The paper has been published in IJCAI'21.

Highlights Conference 2020 Conference Abstract

Automata Tutor v3

  • Jan Kretinsky

We present the third version of Automata Tutor, an online tool for helping teachers and students in large courses on automata and formal languages. It extends massively the functionality of the previous version, which has already been used by thousands of users in dozens of countries. This work will appear in CAV 2020. Although a non-research paper, it targets exactly the Highlights audience, aiming to help in the courses held by many of the attendees.

Highlights Conference 2013 Conference Abstract

Compositional verification and optimization of interactive Markov chains

  • Holger Hermanns
  • Jan Krčál
  • Jan Kretinsky

We provide the first assume-guarantee reasoning for stochastic continuous-time systems. Interactive Markov chains (IMC) are compositional behavioural models similar to continuous-time Markov decision processes. Given a time-bounded property, an IMC component and a specification of the environment, we synthesize a scheduler optimizing the probability that the property is satisfied when the IMC is working in an unknown environment that satisfies the specification. In this talk we focus on a two-player continuous-time stochastic game model that we call controller-environment games that is the crucial step in the solution of the problem above.

Highlights Conference 2013 Conference Abstract

Verification of open interactive Markov chains

  • Tomáš Brázdil
  • Holger Hermanns
  • Jan Krčál
  • Jan Kretinsky
  • Vojtĕch Řehák

We provide the first assume-guarantee reasoning for stochastic continuous-time systems. Interactive Markov chains (IMC) are compositional behavioural models similar to continuous-time Markov decision processes. Given a time-bounded property and an IMC component, we synthesize its scheduler optimizing the probability that the property is satisfied when the IMC is working in an unknown environment. We also give a specification formalism for IMC and consider unknown environments satisfying a given specification.

v2026.09.13