| 2026 | CaiSE | Capturing Processes in Probabilistic Timed Automata. | Harry H. Beyel, Maximilian Prokop, Jan Kretnsk, Giuseppe De Giacomo, Wil M. P. van der Aalst |
| 2026 | CAV | SemML 2.0: Synthesizing Controllers for LTL. | Jan Kretnsk, Tobias Meggendorfer, Maximilian Prokop |
| 2025 | LICS | Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games. | Marta Grobelna, Jan Kretnsk, Maximilian Weininger |
| 2025 | UAI | Symbiotic Local Search for Small Decision Tree Policies in MDPs. | Roman Andriushchenko, Milan Ceska, Debraj Chakraborty, Sebastian Junges, Jan Kretnsk, Filip Mack |
| 2025 | RV | Hidden-Layer Monitoring for Out-of-Distribution Localization in Image Segmentation. | Jan Kretnsk, Sabine Rieder, Gesina Schwalbe, Youssef Shoeb |
| 2025 | SETTA | Keep it Simple, or Teach Them Logics: Attack-Defense Tree Perception by Laypeople. | Florian Dorfhuber, Marisol Barrientos, Julia Eisentraut, Jan Kretnsk |
| 2025 | TACAS | SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning. | Jan Kretnsk, Tobias Meggendorfer, Maximilian Prokop, Ashkan Zarkhah |
| 2025 | VMCAI | 1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization. | Muqsit Azeem, Debraj Chakraborty, Sudeep Kanav, Jan Kretnsk, MohammadSadegh Mohagheghi, Stefanie Mohr, Maximilian Weininger |
| 2024 | CAV | Monitizer: Automating Design and Evaluation of Neural Network Monitors. | Muqsit Azeem, Marta Grobelna, Sudeep Kanav, Jan Kretnsk, Stefanie Mohr, Sabine Rieder |
| 2024 | ECAI | stl2vec: Semantic and Interpretable Vector Representation of Temporal Logic. | Gaia Saveri, Laura Nenzi, Luca Bortolussi, Jan Kretnsk |
| 2024 | RV | Gaussian-Based and Outside-the-Box Runtime Monitoring Join Forces. | Vahid Hashemi, Jan Kretnsk, Sabine Rieder, Torsten Schn, Jan Vorhoff |
| 2024 | TACAS | Learning Explainable and Better Performing Representations of POMDP Strategies. | Alexander Bork, Debraj Chakraborty, Kush Grover, Jan Kretnsk, Stefanie Mohr |
| 2024 | VECoS | Statistical Model Checking the 2024 Edition! | Sudeep Kanav, Jan Kretnsk, Kim G. Larsen |
| 2023 | ATVA | Syntactic vs Semantic Linear Abstraction and Refinement of Neural Networks. | Calvin Chau, Jan Kretnsk, Stefanie Mohr |
| 2023 | CAV | Guessing Winning Policies in LTL Synthesis by Semantic Learning. | Jan Kretnsk, Tobias Meggendorfer, Maximilian Prokop, Sabine Rieder |
| 2023 | FM | Runtime Monitoring for Out-of-Distribution Detection in Object Detection Neural Networks. | Vahid Hashemi, Jan Kretnsk, Sabine Rieder, Jessica Schmidt |
| 2023 | ICTAC | Learning Attack Trees by Genetic Algorithms. | Florian Dorfhuber, Julia Eisentraut, Jan Kretnsk |
| 2023 | LICS | Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives. | Jan Kretnsk, Tobias Meggendorfer, Maximilian Weininger |
| 2023 | VECoS | Welcome Remarks from AISoLA 2023/Track C2 Chairs. | Nils Jansen, Bettina Knighofer, Jan Kretnsk, Kim G. Larsen |
| 2022 | ATVA | Optimistic and Topological Value Iteration for Simple Stochastic Games. | Muqsit Azeem, Alexandros Evangelidis, Jan Kretnsk, Alexander Slivinskiy, Maximilian Weininger |
| 2022 | CAV | PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP. | Chaitanya Agarwal, Shibashis Guha, Jan Kretnsk, Pazhamalai Muruganandham |
| 2022 | CONCUR | Anytime Guarantees for Reachability in Uncountable Markov Decision Processes. | Kush Grover, Jan Kretnsk, Tobias Meggendorfer, Maximilian Weininger |
| 2022 | ICRA | Planning via model checking with decision-tree controllers. | Jonis Kiesbye, Kush Grover, Pranav Ashok, Jan Kretnsk |
| 2022 | TACAS | Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes. | Luca Bortolussi, Giuseppe Maria Gallo, Jan Kretnsk, Laura Nenzi |
| 2021 | CONCUR | Enforcing ω-Regular Properties in Markov Chains by Restarting. | Javier Esparza, Stefan Kiefer, Jan Kretnsk, Maximilian Weininger |
| 2021 | IJCAI | LTL-Constrained Steady-State Policy Synthesis. | Jan Kretnsk |
| 2021 | ICTAC | Assessing Security of Cryptocurrencies with Attack-Defense Trees: Proof of Concept and Future Directions. | Julia Eisentraut, Stephan Holzer, Katharina Klioba, Jan Kretnsk, Lukas Pin, Alexander Wagner |
| 2021 | RV | Gaussian-Based Runtime Detection of Out-of-distribution Inputs for Neural Networks. | Vahid Hashemi, Jan Kretnsk, Stefanie Mohr, Emmanouil Seferis |
| 2021 | TACAS | dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts. | Pranav Ashok, Mathias Jackermeier, Jan Kretnsk, Christoph Weinhuber, Maximilian Weininger, Mayank Yadav |
| 2020 | ATVA | DeepAbstract: Neural Network Abstraction for Accelerating Verification. | Pranav Ashok, Vahid Hashemi, Jan Kretnsk, Stefanie Mohr |
| 2020 | CAV | SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks. | Milan Ceska, Calvin Chau, Jan Kretnsk |
| 2020 | CAV | Automata Tutor v3. | Loris D'Antoni, Martin Helfrich, Jan Kretnsk, Emanuel Ramneantu, Maximilian Weininger |
| 2020 | ISoLA | Statistical Model Checking: Black or White? | Pranav Ashok, Przemyslaw Daca, Jan Kretnsk, Maximilian Weininger |
| 2020 | ISoLA | On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report. | Carlos E. Budde, Arnd Hartmanns, Michaela Klauck, Jan Kretnsk, David Parker, Tim Quatmann, Andrea Turrini, Zhen Zhang |
| 2020 | LICS | Approximating Values of Generalized-Reachability Stochastic Games. | Pranav Ashok, Krishnendu Chatterjee, Jan Kretnsk, Maximilian Weininger, Tobias Winkler |
| 2020 | UAI | Finite-Memory Near-Optimal Learning for Markov Decision Processes with Long-Run Average Reward. | Jan Kretnsk, Fabian Michel, Lukas Michel, Guillermo A. Prez |
| 2019 | ATVA | Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis. | Jan Kretnsk, Alexander Manta, Tobias Meggendorfer |
| 2019 | CAV | PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games. | Pranav Ashok, Jan Kretnsk, Maximilian Weininger |
| 2019 | CAV | Semi-quantitative Abstraction and Analysis of Chemical Reaction Networks. | Milan Ceska, Jan Kretnsk |
| 2019 | CONCUR | Of Cores: A Partial-Exploration Framework for Markov Decision Processes. | Jan Kretnsk, Tobias Meggendorfer |
| 2019 | TACAS | The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report). | Ernst Moritz Hahn, Arnd Hartmanns, Christian Hensel, Michaela Klauck, Joachim Klein, Jan Kretnsk, David Parker, Tim Quatmann, Enno Ruijters, Marcel Steinmetz |
| 2018 | ATVA | Continuous-Time Markov Decisions Based on Partial Exploration. | Pranav Ashok, Yuliya Butkova, Holger Hermanns, Jan Kretnsk |
| 2018 | ATVA | Owl: A Library for ω-Words, Automata, and LTL. | Jan Kretnsk, Tobias Meggendorfer, Salomon Sickert |
| 2018 | CAV | Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm. | Edon Kelmendi, Julia Krmer, Jan Kretnsk, Maximilian Weininger |
| 2018 | CAV | Rabinizer 4: From LTL to Your Favourite Deterministic Automaton. | Jan Kretnsk, Tobias Meggendorfer, Salomon Sickert, Christopher Ziegler |
| 2018 | CONCUR | Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints. | Jan Kretnsk, Guillermo A. Prez, Jean-Franois Raskin |
| 2018 | CONCUR | The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL. | Jan Kretnsk, Alexej Rotar |
| 2018 | ISoLA | Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes. | Pranav Ashok, Toms Brzdil, Jan Kretnsk, Ondrej Slmecka |
| 2018 | LICS | One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata. | Javier Esparza, Jan Kretnsk, Salomon Sickert |
| 2018 | LICS | Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes. | Jan Kretnsk, Tobias Meggendorfer |
| 2018 | TACAS | Strategy Representation by Decision Trees in Reactive Synthesis. | Toms Brzdil, Krishnendu Chatterjee, Jan Kretnsk, Viktor Toman |
| 2017 | ATVA | Efficient Strategy Iteration for Mean Payoff in Markov Decision Processes. | Jan Kretnsk, Tobias Meggendorfer |
| 2017 | CAV | Value Iteration for Long-Run Average Reward in Markov Decision Processes. | Pranav Ashok, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretnsk, Tobias Meggendorfer |
| 2017 | TACAS | From LTL and Limit-Deterministic Bchi Automata to Deterministic Parity Automata. | Javier Esparza, Jan Kretnsk, Jean-Franois Raskin, Salomon Sickert |
| 2017 | TACAS | Index Appearance Record for Transforming Rabin Automata into Parity Automata. | Jan Kretnsk, Tobias Meggendorfer, Clara Waldmann, Maximilian Weininger |
| 2016 | ATVA | MoChiBA: Probabilistic LTL Model Checking Using Limit-Deterministic Bchi Automata. | Salomon Sickert, Jan Kretnsk |
| 2016 | CAV | Limit-Deterministic Bchi Automata for Linear Temporal Logic. | Salomon Sickert, Javier Esparza, Stefan Jaax, Jan Kretnsk |
| 2016 | CONCUR | Linear Distances between Markov Chains. | Przemyslaw Daca, Thomas A. Henzinger, Jan Kretnsk, Tatjana Petrov |
| 2016 | ISoLA | Survey of Statistical Verification of Linear Unbounded Properties: Model Checking and Distances. | Jan Kretnsk |
| 2016 | TACAS | Faster Statistical Model Checking for Unbounded Temporal Properties. | Przemyslaw Daca, Thomas A. Henzinger, Jan Kretnsk, Tatjana Petrov |
| 2015 | CAV | The Hanoi Omega-Automata Format. | Toms Babiak, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Kretnsk, David Mller, David Parker, Jan Strejcek |
| 2015 | CAV | Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. | Toms Brzdil, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner, Jan Kretnsk |
| 2015 | CONCUR | Polynomial Time Decidability of Weighted Synchronization under Partial Observability. | Jan Kretnsk, Kim Guldstrand Larsen, Simon Laursen, Jir Srba |
| 2015 | LICS | Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. | Krishnendu Chatterjee, Zuzana Komrkov, Jan Kretnsk |
| 2015 | LPAR | Controller Synthesis for MDPs and Frequency LTL | Vojtech Forejt, Jan Krcl, Jan Kretnsk |
| 2014 | ATVA | Verification of Markov Decision Processes Using Learning Algorithms. | Toms Brzdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Kretnsk, Marta Z. Kwiatkowska, David Parker, Mateusz Ujma |
| 2014 | ATVA | Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata. | Zuzana Komrkov, Jan Kretnsk |
| 2014 | CAV | From LTL to Deterministic Automata: A Safraless Compositional Approach. | Javier Esparza, Jan Kretnsk |
| 2014 | CONCUR | Probabilistic Bisimulation: Naturally on Distributions. | Holger Hermanns, Jan Krcl, Jan Kretnsk |
| 2013 | ATVA | Rabinizer 2: Small Deterministic Automata for LTL ∖ GU. | Jan Kretnsk, Rusln Ledesma-Garza |
| 2013 | ATVA | MoTraS: A Tool for Modal Transition Systems and Their Extensions. | Jan Kretnsk, Salomon Sickert |
| 2013 | CAV | Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. | Krishnendu Chatterjee, Andreas Gaiser, Jan Kretnsk |
| 2013 | CONCUR | Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory. | Nikola Benes, Benot Delahaye, Uli Fahrenberg, Jan Kretnsk, Axel Legay |
| 2013 | CONCUR | Compositional Verification and Optimization of Interactive Markov Chains. | Holger Hermanns, Jan Krcl, Jan Kretnsk |
| 2013 | ICTAC | On Refinements of Boolean and Parametric Modal Transition Systems. | Jan Kretnsk, Salomon Sickert |
| 2012 | ATVA | Rabinizer: Small Deterministic Automata for LTL(F, G). | Andreas Gaiser, Jan Kretnsk, Javier Esparza |
| 2012 | CAV | Deterministic Automata for the (F, G)-Fragment of LTL. | Jan Kretnsk, Javier Esparza |
| 2012 | ICTAC | Modal Process Rewrite Systems. | Nikola Benes, Jan Kretnsk |
| 2012 | LPAR | Dual-Priced Modal Transition Systems with Time Durations. | Nikola Benes, Jan Kretnsk, Kim Guldstrand Larsen, Mikael H. Mller, Jir Srba |
| 2011 | ATVA | Modal Transition Systems: Composition and LTL Model Checking. | Nikola Benes, Ivana Cern, Jan Kretnsk |
| 2011 | ATVA | Parametric Modal Transition Systems. | Nikola Benes, Jan Kretnsk, Kim G. Larsen, Mikael H. Mller, Jir Srba |
| 2011 | CONCUR | Fixed-Delay Events in Generalized Semi-Markov Processes Revisited. | Toms Brzdil, Jan Krcl, Jan Kretnsk, Vojtech Rehk |
| 2010 | CONCUR | Stochastic Real-Time Games with Qualitative Timed Automata Objectives. | Toms Brzdil, Jan Krcl, Jan Kretnsk, Antonn Kucera, Vojtech Rehk |
| 2009 | ICTAC | Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete. | Nikola Benes, Jan Kretnsk, Kim Guldstrand Larsen, Jir Srba |
| 2008 | LICS | The Satisfiability Problem for Probabilistic CTL. | Toms Brzdil, Vojtech Forejt, Jan Kretnsk, Antonn Kucera |