E-Mail: firstname.lastname@tum.de
ORCID:
0000-0002-8122-2881Address:
Botanická 554/68a, 602 00 Brno
Jan Křetínský
Office: C514
E-Mail: firstname.lastname@tum.de
ORCID: 0000-0002-8122-2881
Address:
E-Mail: firstname.lastname@tum.de
ORCID:
0000-0002-8122-2881Address:
Research Areas
Value Iteration for Stochastic Games
We develop value iteration algorithms for stochastic games.
Runtime Monitoring of Neural Network
We develop runtime monitors for neural networks to improve their reliability.
Abstraction of Neural Network
We abstract neural networks to improve verification speed.
Machine Learning for LTL Synthesis
We apply machine learning to the LTL synthesis problem.
Translating LTL to Automata
We design algorithms for translating LTL to different types of automata.
Explaining Controllers via Decision Trees
We develop methods for explaining controllers with decision trees.
Explaining Controllers via Automata
We develop methods for explaining controllers via automata.
Concurrent Stochastic Games
We develop techniques for the verification of concurrent stochastic games which extend turn-based stochastic games by allowing players to select actions simultaneously in each state, reflecting more realistic scenarios of interactive agents acting concurrently.
Tools
SemML
In this project we develop learning-based exploration heuristics for LTL Synthesis that exploit the semantic labelling of the underlying Automaton/Game.
MONITIZER
We create a tool (Monitizer) that optimizes monitors on a NN for a specific task.
dtControl
Represent controllers as decision trees. Improve memory footprint, boost explainability while preserving guarantees.
Automata Tutor is an online teaching tool that aids instructors and students in large courses on automata and formal languages with many different exercise types.