Author name cluster

Jan Kretí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.

6 papers

1 author row

UAI Conference 2025 Conference Paper

Symbiotic Local Search for Small Decision Tree Policies in MDPs

Roman Andriushchenko
Milan Ceska 0002
Debraj Chakraborty 0002
Sebastian Junges
Jan Kretínský
Filip Macák

We study decision making policies in Markov decision processes (MDPs). Two key performance indicators of such policies are their value and their interpretability. On the one hand, policies that optimize value can be efficiently computed via a plethora of standard methods. However, the representation of these policies may prevent their interpretability. On the other hand, policies with good interpretability, such as policies represented by a small decision tree, are computationally hard to obtain. This paper contributes a local search approach to find policies with good value, represented by small decision trees. Our local search symbiotically combines learning decision trees from value-optimal policies with symbolic approaches that optimize the size of the decision tree within a constrained neighborhood. Our empirical evaluation shows that this combination provides drastically smaller decision trees for MDPs that are significantly larger than what can be handled by optimal decision tree learners.

Details

ECAI Conference 2024 Conference Paper

stl2vec: Semantic and Interpretable Vector Representation of Temporal Logic

Gaia Saveri
Laura Nenzi
Luca Bortolussi
Jan Kretínský

Integrating symbolic knowledge and data-driven learning algorithms is a longstanding challenge in Artificial Intelligence. Despite the recognized importance of this task, a notable gap exists due to the discreteness of symbolic representations and the continuous nature of machine-learning computations. One of the desired bridges between these two worlds would be to define semantically grounded vector representation (feature embedding) of logic formulae, thus enabling to perform continuous learning and optimization in the semantic space of formulae. We tackle this goal for knowledge expressed in Signal Temporal Logic (STL) and devise a method to compute continuous embeddings of formulae with several desirable properties: the embedding (i) is finite-dimensional, (ii) faithfully reflects the semantics of the formulae, (iii) does not require any learning but instead is defined from basic principles, (iv) is interpretable. Another significant contribution lies in demonstrating the efficacy of the approach in two tasks: learning model checking, where we predict the probability of requirements being satisfied in stochastic processes; and integrating the embeddings into a neuro-symbolic framework, to constrain the output of a deep-learning generative model to comply to a given logical specification.

Details

ICRA Conference 2022 Conference Paper

Planning via model checking with decision-tree controllers

Jonis Kiesbye
Kush Grover
Pranav Ashok
Jan Kretínský

Planning problems can be solved not only by planners, but also by model checkers. While the former yield a plan that requires replanning as soon as any fault occurs, the latter provide a “universal” plan (a. k. a. strategy, policy, or controller) able to make decisions under all circumstances. One of the prohibitive aspects of the latter approach is stemming from this very advantage: since it is defined for all possible states of the system, it is typically so large that it does not fit into small memories of embedded devices. As another consequence of the size, its execution may be slow. In this paper, we provide a solution to this issue by linking the model checkers with decision-tree learners, resulting in decision-tree representations of the synthesized strategies. Not only are they dramatically smaller, but also more explainable and orders-of-magnitude faster to execute than plans with replanning. In addition, we describe a method for model validation and debugging via the model checker and the decision-tree learner in the loop. We illustrate the approach on our case study of a robotic arm for picking items in a real industrial setting.

Details

UAI Conference 2020 Conference Paper

Finite-Memory Near-Optimal Learning for Markov Decision Processes with Long-Run Average Reward

Jan Kretínský
Fabian Michel
Lukas Michel
Guillermo A. Pérez

We consider learning policies online in Markov decision processes with the long-run average reward (a. k. a. mean payoff). To ensure implementability of the policies, we focus on policies with finite memory. Firstly, we show that near optimality can be achieved almost surely, using an unintuitive gadget we call forgetfulness. Secondly, we extend the approach to a setting with partial knowledge of the system topology, introducing two optimality measures and providing near-optimal algorithms also for these cases.

Details

LPAR Conference 2015 Conference Paper

Controller Synthesis for MDPs and Frequency LTL \GU

Vojtech Forejt
Jan Krcál
Jan Kretínský

Abstract Quantitative extensions of temporal logics have recently attracted significant attention. In this work, we study frequency LTL (fLTL), an extension of LTL which allows to speak about frequencies of events along an execution. Such an extension is particularly useful for probabilistic systems that often cannot fulfil strict qualitative guarantees on the behaviour. It has been recently shown that controller synthesis for Markov decision processes and fLTL is decidable when all the bounds on frequencies are 1. As a step towards a complete quantitative solution, we show that the problem is decidable for the fragment \({{\text {fLTL}_{\setminus \mathbf{G}\mathbf U}}}\), where \(\mathbf U\) does not occur in the scope of \(\mathbf{G}\) (but still \(\mathbf{F}\) can). Our solution is based on a novel translation of such quantitative formulae into equivalent deterministic automata.

Details

LPAR Conference 2012 Conference Paper

Dual-Priced Modal Transition Systems with Time Durations

Nikola Benes
Jan Kretínský
Kim G. Larsen
Mikael H. Møller
Jirí Srba

Abstract Modal transition systems are a well-established specification formalism for a high-level modelling of component-based software systems. We present a novel extension of the formalism called modal transition systems with durations where time durations are modelled as controllable or uncontrollable intervals. We further equip the model with two kinds of quantitative aspects: each action has its own running cost per time unit, and actions may require several hardware components of different costs. We ask the question, given a fixed budget for the hardware components, what is the implementation with the cheapest long-run average reward. We give an algorithm for computing such optimal implementations via a reduction to a new extension of mean payoff games with time durations and analyse the complexity of the algorithm.

Details