Jan Kretínský

210 papers A* 12A 4B 33C 5Journal 98Unranked 56
YearRankTypeTitle / Venue / Authors
2026 J jnl
Provably Explaining Neural Additive Models.
CoRR
Shahaf Bassan, Yizhak Yisrael Elboher, Tobias Ladner, Volkan Sahin, Jan Kretínský, Matthias Althoff, Guy Katz
2026 J jnl
Resilient Strategies for Stochastic Systems: How Much Does It Take to Break a Winning Strategy?
CoRR
Kush Grover, Markel Zubia, Debraj Chakraborty, Muqsit Azeem, Nils Jansen, Jan Kretínský
2026 J jnl
Semantically Labelled Automata for Multi-Task Reinforcement Learning with LTL Instructions.
CoRR
Alessandro Abate, Giuseppe De Giacomo, Mathias Jackermeier, Jan Kretínský, Maximilian Prokop, Christoph Weinhuber
2026 J jnl
Talking with Verifiers: Automatic Specification Generation for Neural Network Verification.
CoRR
Yizhak Yisrael Elboher, Reuven Peleg, Zhouxing Shi, Guy Katz, Jan Kretínský
2025 — conf
1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization.
VMCAI (2)
Muqsit Azeem, Debraj Chakraborty, Sudeep Kanav, Jan Kretínský, MohammadSadegh Mohagheghi, Stefanie Mohr, Maximilian Weininger
2025 — conf
Explaining Control Policies through Predicate Decision Diagrams.
HSCC
Debraj Chakraborty, Clemens Dubslaff, Sudeep Kanav, Jan Kretínský, Christoph Weinhuber
2025 J jnl
Explaining Control Policies through Predicate Decision Diagrams.
CoRR
Debraj Chakraborty, Clemens Dubslaff, Sudeep Kanav, Jan Kretínský, Christoph Weinhuber
2025 B conf
Hidden-Layer Monitoring for Out-of-Distribution Localization in Image Segmentation.
RV
Jan Kretínský, Sabine Rieder, Gesina Schwalbe, Youssef Shoeb
2025 J jnl
Learning Algorithms for Verification of Markov Decision Processes.
TheoretiCS
Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Kretínský, Marta Kwiatkowska, Tobias Meggendorfer, David Parker, Mateusz Ujma
2025 J jnl
PAC statistical model checking of mean payoff in discrete- and continuous-time MDP.
Formal Methods Syst. Des.
Chaitanya Agarwal, Shibashis Guha, Jan Kretínský, M. Pazhamalai
2025 — conf
SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning.
TACAS (1)
Jan Kretínský, Tobias Meggendorfer, Maximilian Prokop, Ashkan Zarkhah
2025 J jnl
SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning.
CoRR
Jan Kretínský, Tobias Meggendorfer, Maximilian Prokop, Ashkan Zarkhah
2025 — conf
Sound Value Iteration for Simple Stochastic Games.
GandALF
Muqsit Azeem, Jan Kretínský, Maximilian Weininger
2025 A* conf
Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games.
LICS
Marta Grobelna, Jan Kretínský, Maximilian Weininger
2025 J jnl
Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games.
CoRR
Marta Grobelna, Jan Kretínský, Maximilian Weininger
2025 A conf
Symbiotic Local Search for Small Decision Tree Policies in MDPs.
UAI
Roman Andriushchenko, Milan Ceska, Debraj Chakraborty, Sebastian Junges, Jan Kretínský, Filip Macák
2024 J jnl
1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization.
CoRR
Muqsit Azeem, Debraj Chakraborty, Sudeep Kanav, Jan Kretínský, MohammadSadegh Mohagheghi, Stefanie Mohr, Maximilian Weininger
2024 — conf
A Literature Review on Verification and Abstraction of Neural Networks Within the Formal Methods Community.
Principles of Verification (3)
Sudeep Kanav, Jan Kretínský, Sabine Rieder
2024 J jnl
Abstraction-based segmental simulation of reaction networks using adaptive memoization.
BMC Bioinform.
Martin Helfrich, Roman Andriushchenko, Milan Ceska, Jan Kretínský, Stefan Marticek, David Safránek
2024 J jnl
Artificial Intelligence and Formal Methods Join Forces for Reliable Autonomy (Dagstuhl Seminar 24361).
Dagstuhl Reports
Nils Jansen, Mykel J. Kochenderfer, Jan Kretínský, Jana Tumova, Maris F. L. Galesloot
2024 J jnl
Explainable Finite-Memory Policies for Partially Observable Markov Decision Processes.
CoRR
Muqsit Azeem, Debraj Chakraborty, Sudeep Kanav, Jan Kretínský
2024 B conf
Gaussian-Based and Outside-the-Box Runtime Monitoring Join Forces.
RV
Vahid Hashemi, Jan Kretínský, Sabine Rieder, Torsten Schön, Jan Vorhoff
2024 J jnl
Gaussian-Based and Outside-the-Box Runtime Monitoring Join Forces.
CoRR
Vahid Hashemi, Jan Kretínský, Sabine Rieder, Torsten Schön, Jan Vorhoff
2024 J jnl
Learning Algorithms for Verification of Markov Decision Processes.
CoRR
Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Kretínský, Marta Kwiatkowska, Tobias Meggendorfer, David Parker, Mateusz Ujma
2024 — conf
Learning Explainable and Better Performing Representations of POMDP Strategies.
TACAS (2)
Alexander Bork, Debraj Chakraborty, Kush Grover, Jan Kretínský, Stefanie Mohr
2024 J jnl
Learning Explainable and Better Performing Representations of POMDP Strategies.
CoRR
Alexander Bork, Debraj Chakraborty, Kush Grover, Jan Kretínský, Stefanie Mohr
2024 — conf
MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints✱.
HSCC
Severin Bals, Alexandros Evangelidis, Jan Kretínský, Jakob Waibel
2024 — conf
Monitizer: Automating Design and Evaluation of Neural Network Monitors.
CAV (2)
Muqsit Azeem, Marta Grobelna, Sudeep Kanav, Jan Kretínský, Stefanie Mohr, Sabine Rieder
2024 J jnl
Monitizer: Automating Design and Evaluation of Neural Network Monitors.
CoRR
Muqsit Azeem, Marta Grobelna, Sudeep Kanav, Jan Kretínský, Stefanie Mohr, Sabine Rieder
2024 — conf
Poster Abstract: MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints✱.
HSCC
Severin Bals, Alexandros Evangelidis, Jan Kretínský, Jakob Waibel
2024 — conf
QuADTool: Attack-Defense-Tree Synthesis, Analysis and Bridge to Verification.
QEST+FORMATS
Florian Dorfhuber, Julia Eisentraut, Katharina Klioba, Jan Kretínský
2024 J jnl
QuADTool: Attack-Defense-Tree Synthesis, Analysis and Bridge to Verification.
CoRR
Florian Dorfhuber, Julia Eisentraut, Katharina Klioba, Jan Kretínský
2024 J jnl
Sound Value Iteration for Simple Stochastic Games.
CoRR
Muqsit Azeem, Jan Kretínský, Maximilian Weininger
2024 — conf
Statistical Model Checking the 2024 Edition!
AISoLA
Sudeep Kanav, Jan Kretínský, Kim G. Larsen
2024 J jnl
Stochastic Games (Dagstuhl Seminar 24231).
Dagstuhl Reports
Nathanaël Fijalkow, Jan Kretínský, Ann Nowé, Gabriel Bathie
2024 — ed.
Taming the Infinities of Concurrency - Essays Dedicated to Javier Esparza on the Occasion of His 60th Birthday
Taming the Infinities of Concurrency
Stefan Kiefer, Jan Kretínský, Antonín Kucera
2024 J jnl
Tools at the Frontiers of Quantitative Verification.
CoRR
Roman Andriushchenko, Alexander Bork, Carlos E. Budde, Milan Ceska, Kush Grover, Ernst Moritz Hahn, Arnd Hartmanns, Bryant Israelsen, Nils Jansen, Joshua Jeppson, Sebastian Junges, Maximilian A. Köhl, Bettina Könighofer, Jan Kretínský, Tobias Meggendorfer, David Parker, Stefan Pranger, Tim Quatmann, Enno Ruijters, Landon Taylor, Matthias Volk, Maximilian Weininger, Zhen Zhang
2024 A conf
stl2vec: Semantic and Interpretable Vector Representation of Temporal Logic.
ECAI
Gaia Saveri, Laura Nenzi, Luca Bortolussi, Jan Kretínský
2024 J jnl
stl2vec: Semantic and Interpretable Vector Representation of Temporal Logic.
CoRR
Gaia Saveri, Laura Nenzi, Luca Bortolussi, Jan Kretínský
2023 J jnl
Algebraically explainable controllers: decision trees and support vector machines join forces.
Int. J. Softw. Tools Technol. Transf.
Florian Jüngermann, Jan Kretínský, Maximilian Weininger
2023 — conf
Guessing Winning Policies in LTL Synthesis by Semantic Learning.
CAV (1)
Jan Kretínský, Tobias Meggendorfer, Maximilian Prokop, Sabine Rieder
2023 J jnl
Guessing Winning Policies in LTL Synthesis by Semantic Learning.
CoRR
Jan Kretínský, Tobias Meggendorfer, Maximilian Prokop, Sabine Rieder
2023 C conf
Learning Attack Trees by Genetic Algorithms.
ICTAC
Florian Dorfhuber, Julia Eisentraut, Jan Kretínský
2023 J jnl
MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints.
CoRR
Severin Bals, Alexandros Evangelidis, Kush Grover, Jan Kretínský, Jakob Waibel
2023 B conf
Runtime Monitoring for Out-of-Distribution Detection in Object Detection Neural Networks.
FM
Vahid Hashemi, Jan Kretínský, Sabine Rieder, Jessica Schmidt
2023 A* conf
Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives.
LICS
Jan Kretínský, Tobias Meggendorfer, Maximilian Weininger
2023 J jnl
Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives.
CoRR
Jan Kretínský, Tobias Meggendorfer, Maximilian Weininger
2023 — conf
Syntactic vs Semantic Linear Abstraction and Refinement of Neural Networks.
ATVA (1)
Calvin Chau, Jan Kretínský, Stefanie Mohr
2023 J jnl
Syntactic vs Semantic Linear Abstraction and Refinement of Neural Networks.
CoRR
Calvin Chau, Jan Kretínský, Stefanie Mohr
2023 — conf
Tools at the Frontiers of Quantitative Verification - QComp 2023 Competition Report.
TOOLympics@ETAPS
Roman Andriushchenko, Alexander Bork, Carlos E. Budde, Milan Ceska, Kush Grover, Ernst Moritz Hahn, Arnd Hartmanns, Bryant Israelsen, Nils Jansen, Joshua Jeppson, Sebastian Junges, Maximilian A. Köhl, Bettina Könighofer, Jan Kretínský, Tobias Meggendorfer, David Parker, Stefan Pranger, Tim Quatmann, Enno Ruijters, Landon Taylor, Matthias Volk, Maximilian Weininger, Zhen Zhang
2023 — conf
Welcome Remarks from AISoLA 2023/Track C2 Chairs.
AISoLA
Nils Jansen, Bettina Könighofer, Jan Kretínský, Kim G. Larsen
2022 — conf
Abstraction-Based Segmental Simulation of Chemical Reaction Networks.
CMSB
Martin Helfrich, Milan Ceska, Jan Kretínský, Stefan Marticek
2022 J jnl
Abstraction-Based Segmental Simulation of Chemical Reaction Networks.
CoRR
Martin Helfrich, Milan Ceska, Jan Kretínský, Stefan Marticek
2022 J jnl
Algebraically Explainable Controllers: Decision Trees and Support Vector Machines Join Forces.
CoRR
Florian Jüngermann, Jan Kretínský, Maximilian Weininger
2022 B conf
Anytime Guarantees for Reachability in Uncountable Markov Decision Processes.
CONCUR
Kush Grover, Jan Kretínský, Tobias Meggendorfer, Maximilian Weininger
2022 J jnl
Comparison of algorithms for simple stochastic games.
Inf. Comput.
Jan Kretínský, Emanuel Ramneantu, Alexander Slivinskiy, Maximilian Weininger
2022 J jnl
From linear temporal logic and limit-deterministic Büchi automata to deterministic parity automata.
Int. J. Softw. Tools Technol. Transf.
Javier Esparza, Jan Kretínský, Jean-François Raskin, Salomon Sickert
2022 J jnl
Index appearance record with preorders.
Acta Informatica
Jan Kretínský, Tobias Meggendorfer, Clara Waldmann, Maximilian Weininger
2022 — conf
Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes.
TACAS (1)
Luca Bortolussi, Giuseppe Maria Gallo, Jan Kretínský, Laura Nenzi
2022 J jnl
Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes.
CoRR
Luca Bortolussi, Giuseppe Maria Gallo, Jan Kretínský, Laura Nenzi
2022 B conf
Optimistic and Topological Value Iteration for Simple Stochastic Games.
ATVA
Muqsit Azeem, Alexandros Evangelidis, Jan Kretínský, Alexander Slivinskiy, Maximilian Weininger
2022 J jnl
Optimistic and Topological Value Iteration for Simple Stochastic Games.
CoRR
Muqsit Azeem, Alexandros Evangelidis, Jan Kretínský, Alexander Slivinskiy, Maximilian Weininger
2022 — conf
PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP.
CAV (2)
Chaitanya Agarwal, Shibashis Guha, Jan Kretínský, Pazhamalai Muruganandham
2022 J jnl
PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP.
CoRR
Chaitanya Agarwal, Shibashis Guha, Jan Kretínský, M. Pazhamalai
2022 A* conf
Planning via model checking with decision-tree controllers.
ICRA
Jonis Kiesbye, Kush Grover, Pranav Ashok, Jan Kretínský
2022 J jnl
Runtime Monitoring for Out-of-Distribution Detection in Object Detection Neural Networks.
CoRR
Vahid Hashemi, Jan Kretínský, Sabine Rieder, Jessica Schmidt
2022 J jnl
Satisfiability Bounds for ω-Regular Properties in Bounded-Parameter Markov Decision Processes.
CoRR
Jan Kretínský, Tobias Meggendorfer, Maximilian Weininger
2022 — conf
Satisfiability of Quantitative Probabilistic CTL: Rise to the Challenge.
Principles of Systems Design
Miroslav Chodil, Antonín Kucera, Jan Kretínský
2022 J jnl
Value iteration for simple stochastic games: Stopping criterion and learning algorithm.
Inf. Comput.
Julia Eisentraut, Edon Kelmendi, Jan Kretínský, Maximilian Weininger
2021 C conf
Assessing Security of Cryptocurrencies with Attack-Defense Trees: Proof of Concept and Future Directions.
ICTAC
Julia Eisentraut, Stephan Holzer, Katharina Klioba, Jan Kretínský, Lukas Pin, Alexander Wagner
2021 B conf
Enforcing ω-Regular Properties in Markov Chains by Restarting.
CONCUR
Javier Esparza, Stefan Kiefer, Jan Kretínský, Maximilian Weininger
2021 J jnl
Formalizing and guaranteeing human-robot interaction.
Commun. ACM
Hadas Kress-Gazit, Kerstin Eder, Guy Hoffman, Henny Admoni, Brenna Argall, Rüdiger Ehlers, Christoffer Heckman, Nils Jansen, Ross A. Knepper, Jan Kretínský, Shelly Levy-Tzedek, Jamy Li, Todd D. Murphey, Laurel D. Riek, Dorsa Sadigh
2021 B conf
Gaussian-Based Runtime Detection of Out-of-distribution Inputs for Neural Networks.
RV
Vahid Hashemi, Jan Kretínský, Stefanie Mohr, Emmanouil Seferis
2021 — conf
Guaranteed Trade-Offs in Dynamic Information Flow Tracking Games.
CDC
Maximilian Weininger, Kush Grover, Shruti Misra, Jan Kretínský
2021 A* conf
LTL-Constrained Steady-State Policy Synthesis.
IJCAI
Jan Kretínský
2021 J jnl
LTL-Constrained Steady-State Policy Synthesis.
CoRR
Jan Kretínský
2021 — conf
Semantic Abstraction-Guided Motion Planning for scLTL Missions in Unknown Environments.
Robotics: Science and Systems
Kush Grover, Fernando S. Barbosa, Jana Tumova, Jan Kretínský
2021 — conf
dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts.
TACAS (2)
Pranav Ashok, Mathias Jackermeier, Jan Kretínský, Christoph Weinhuber, Maximilian Weininger, Mayank Yadav
2021 J jnl
dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts.
CoRR
Pranav Ashok, Mathias Jackermeier, Jan Kretínský, Christoph Weinhuber, Maximilian Weininger, Mayank Yadav
2020 J jnl
A Unified Translation of Linear Temporal Logic to ω-Automata.
J. ACM
Javier Esparza, Jan Kretínský, Salomon Sickert
2020 J jnl
An Anytime Algorithm for Reachability on Uncountable MDP.
CoRR
Kush Grover, Jan Kretínský, Tobias Meggendorfer, Maximilian Weininger
2020 A* conf
Approximating Values of Generalized-Reachability Stochastic Games.
LICS
Pranav Ashok, Krishnendu Chatterjee, Jan Kretínský, Maximilian Weininger, Tobias Winkler
2020 — conf
Automata Tutor v3.
CAV (2)
Loris D'Antoni, Martin Helfrich, Jan Kretínský, Emanuel Ramneantu, Maximilian Weininger
2020 J jnl
Automata Tutor v3.
CoRR
Loris D'Antoni, Martin Helfrich, Jan Kretínský, Emanuel Ramneantu, Maximilian Weininger
2020 J jnl
Comparison of Algorithms for Simple Stochastic Games (Full Version).
CoRR
Jan Kretínský, Emanuel Ramneantu, Alexander Slivinskiy, Maximilian Weininger
2020 — conf
Comparison of Algorithms for Simple Stochastic Games.
GandALF
Jan Kretínský, Emanuel Ramneantu, Alexander Slivinskiy, Maximilian Weininger
2020 B conf
DeepAbstract: Neural Network Abstraction for Accelerating Verification.
ATVA
Pranav Ashok, Vahid Hashemi, Jan Kretínský, Stefanie Mohr
2020 J jnl
DeepAbstract: Neural Network Abstraction for Accelerating Verification.
CoRR
Pranav Ashok, Vahid Hashemi, Jan Kretínský, Stefanie Mohr
2020 A conf
Finite-Memory Near-Optimal Learning for Markov Decision Processes with Long-Run Average Reward.
UAI
Jan Kretínský, Fabian Michel, Lukas Michel, Guillermo A. Pérez
2020 J jnl
Formalizing and Guaranteeing* Human-Robot Interaction.
CoRR
Hadas Kress-Gazit, Kerstin Eder, Guy Hoffman, Henny Admoni, Brenna Argall, Rüdiger Ehlers, Christoffer Heckman, Nils Jansen, Ross A. Knepper, Jan Kretínský, Shelly Levy-Tzedek, Jamy Li, Todd D. Murphey, Laurel D. Riek, Dorsa Sadigh
2020 J jnl
Logical vs. behavioural specifications.
Inf. Comput.
Nikola Benes, Uli Fahrenberg, Jan Kretínský, Axel Legay, Louis-Marie Traonouez
2020 J jnl
Of Cores: A Partial-Exploration Framework for Markov Decision Processes.
Log. Methods Comput. Sci.
Jan Kretínský, Tobias Meggendorfer
2020 — conf
On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report.
ISoLA (4)
Carlos E. Budde, Arnd Hartmanns, Michaela Klauck, Jan Kretínský, David Parker, Tim Quatmann, Andrea Turrini, Zhen Zhang
2020 J jnl
Online Monitoring ω-Regular Properties in Unknown Markov Chains.
CoRR
Javier Esparza, Stefan Kiefer, Jan Kretínský, Maximilian Weininger
2020 — conf
SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks.
CAV (1)
Milan Ceska, Calvin Chau, Jan Kretínský
2020 — conf
Statistical Model Checking: Black or White?
ISoLA (1)
Pranav Ashok, Przemyslaw Daca, Jan Kretínský, Maximilian Weininger
2020 J jnl
dtControl: Decision Tree Learning Algorithms for Controller Representation.
CoRR
Pranav Ashok, Mathias Jackermeier, Pushpak Jagtap, Jan Kretínský, Maximilian Weininger, Majid Zamani
2020 — conf
dtControl: decision tree learning algorithms for controller representation.
HSCC
Pranav Ashok, Mathias Jackermeier, Pushpak Jagtap, Jan Kretínský, Maximilian Weininger, Majid Zamani
2020 — conf
dtControl: decision tree learning algorithms for controller representation.
HSCC
Pranav Ashok, Mathias Jackermeier, Pushpak Jagtap, Jan Kretínský, Maximilian Weininger, Majid Zamani
2019 J jnl
Approximating Values of Generalized-Reachability Stochastic Games.
CoRR
Pranav Ashok, Jan Kretínský, Maximilian Weininger
2019 — conf
Expected Cost Analysis of Attack-Defense Trees.
QEST
Julia Eisentraut, Jan Kretínský
2019 B conf
Of Cores: A Partial-Exploration Framework for Markov Decision Processes.
CONCUR
Jan Kretínský, Tobias Meggendorfer
2019 J jnl
Of Cores: A Partial-Exploration Framework for Markov Decision Processes.
CoRR
Jan Kretínský, Tobias Meggendorfer
2019 — conf
PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games.
CAV (1)
Pranav Ashok, Jan Kretínský, Maximilian Weininger
2019 J jnl
PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games.
CoRR
Pranav Ashok, Jan Kretínský, Maximilian Weininger
2019 — conf
SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processes.
QEST
Pranav Ashok, Jan Kretínský, Kim Guldstrand Larsen, Adrien Le Coënt, Jakob Haahr Taankvist, Maximilian Weininger
2019 J jnl
SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processes.
CoRR
Pranav Ashok, Jan Kretínský, Kim Guldstrand Larsen, Adrien Le Coënt, Jakob Haahr Taankvist, Maximilian Weininger
2019 — conf
Satisfiability Bounds for ω-Regular Properties in Bounded-Parameter Markov Decision Processes.
CDC
Maximilian Weininger, Tobias Meggendorfer, Jan Kretínský
2019 B conf
Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis.
ATVA
Jan Kretínský, Alexander Manta, Tobias Meggendorfer
2019 J jnl
Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis.
CoRR
Jan Kretínský, Alexander Manta, Tobias Meggendorfer
2019 J jnl
Semi-Quantitative Abstraction and Analysis of Chemical Reaction Networks.
CoRR
Milan Ceska, Jan Kretínský
2019 — conf
Semi-quantitative Abstraction and Analysis of Chemical Reaction Networks (Extended Abstract).
CMSB
Milan Ceska, Jan Kretínský
2019 — conf
Semi-quantitative Abstraction and Analysis of Chemical Reaction Networks.
CAV (1)
Milan Ceska, Jan Kretínský
2019 J jnl
Stopping Criteria for Value and Strategy Iteration on Concurrent Stochastic Reachability Games.
CoRR
Julia Eisentraut, Jan Kretínský, Alexej Rotar
2019 — conf
Strategy Representation by Decision Trees with Linear Classifiers.
QEST
Pranav Ashok, Tomás Brázdil, Krishnendu Chatterjee, Jan Kretínský, Christoph H. Lampert, Viktor Toman
2019 J jnl
Strategy Representation by Decision Trees with Linear Classifiers.
CoRR
Pranav Ashok, Tomás Brázdil, Krishnendu Chatterjee, Jan Kretínský, Christoph H. Lampert, Viktor Toman
2019 — conf
The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report).
TACAS (3)
Ernst Moritz Hahn, Arnd Hartmanns, Christian Hensel, Michaela Klauck, Joachim Klein, Jan Kretínský, David Parker, Tim Quatmann, Enno Ruijters, Marcel Steinmetz
2018 J jnl
Compositionality for quantitative specifications.
Soft Comput.
Uli Fahrenberg, Jan Kretínský, Axel Legay, Louis-Marie Traonouez
2018 A* conf
Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes.
LICS
Jan Kretínský, Tobias Meggendorfer
2018 J jnl
Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes.
CoRR
Jan Kretínský, Tobias Meggendorfer
2018 B conf
Continuous-Time Markov Decisions Based on Partial Exploration.
ATVA
Pranav Ashok, Yuliya Butkova, Holger Hermanns, Jan Kretínský
2018 J jnl
Continuous-Time Markov Decisions based on Partial Exploration.
CoRR
Pranav Ashok, Yuliya Butkova, Holger Hermanns, Jan Kretínský
2018 J jnl
LTL Store: Repository of LTL formulae from literature and case studies.
CoRR
Jan Kretínský, Tobias Meggendorfer, Salomon Sickert
2018 B conf
Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints.
CONCUR
Jan Kretínský, Guillermo A. Pérez, Jean-François Raskin
2018 J jnl
Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints.
CoRR
Jan Kretínský, Guillermo A. Pérez, Jean-François Raskin
2018 J jnl
Machine Learning and Model Checking Join Forces (Dagstuhl Seminar 18121).
Dagstuhl Reports
Nils Jansen, Joost-Pieter Katoen, Pushmeet Kohli, Jan Kretínský
2018 — conf
Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes.
ISoLA (2)
Pranav Ashok, Tomás Brázdil, Jan Kretínský, Ondrej Slámecka
2018 J jnl
Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes.
CoRR
Pranav Ashok, Tomás Brázdil, Jan Kretínský, Ondrej Slámecka
2018 A* conf
One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata.
LICS
Javier Esparza, Jan Kretínský, Salomon Sickert
2018 J jnl
One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata.
CoRR
Javier Esparza, Jan Kretínský, Salomon Sickert
2018 B conf
Owl: A Library for ω-Words, Automata, and LTL.
ATVA
Jan Kretínský, Tobias Meggendorfer, Salomon Sickert
2018 — conf
Rabinizer 4: From LTL to Your Favourite Deterministic Automaton.
CAV (1)
Jan Kretínský, Tobias Meggendorfer, Salomon Sickert, Christopher Ziegler
2018 — conf
Strategy Representation by Decision Trees in Reactive Synthesis.
TACAS (1)
Tomás Brázdil, Krishnendu Chatterjee, Jan Kretínský, Viktor Toman
2018 J jnl
Strategy Representation by Decision Trees in Reactive Synthesis.
CoRR
Tomás Brázdil, Krishnendu Chatterjee, Jan Kretínský, Viktor Toman
2018 B conf
The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL.
CONCUR
Jan Kretínský, Alexej Rotar
2018 J jnl
The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL.
CoRR
Jan Kretínský, Alexej Rotar
2018 — conf
Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm.
CAV (1)
Edon Kelmendi, Julia Krämer, Jan Kretínský, Maximilian Weininger
2018 J jnl
Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm.
CoRR
Edon Kelmendi, Julia Krämer, Jan Kretínský, Maximilian Weininger
2017 — conf
30 Years of Modal Transition Systems: Survey of Extensions and Analysis.
Models, Algorithms, Logics and Tools
Jan Kretínský
2017 B conf
Efficient Strategy Iteration for Mean Payoff in Markov Decision Processes.
ATVA
Jan Kretínský, Tobias Meggendorfer
2017 J jnl
Efficient Strategy Iteration for Mean Payoff in Markov Decision Processes.
CoRR
Jan Kretínský, Tobias Meggendorfer
2017 J jnl
Faster Statistical Model Checking for Unbounded Temporal Properties.
ACM Trans. Comput. Log.
Przemyslaw Daca, Thomas A. Henzinger, Jan Kretínský, Tatjana Petrov
2017 — conf
From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata.
TACAS (1)
Javier Esparza, Jan Kretínský, Jean-François Raskin, Salomon Sickert
2017 J jnl
From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata.
CoRR
Javier Esparza, Jan Kretínský, Jean-François Raskin, Salomon Sickert
2017 — conf
Index Appearance Record for Transforming Rabin Automata into Parity Automata.
TACAS (1)
Jan Kretínský, Tobias Meggendorfer, Clara Waldmann, Maximilian Weininger
2017 J jnl
Index appearance record for transforming Rabin automata into parity automata.
CoRR
Jan Kretínský, Tobias Meggendorfer, Clara Waldmann, Maximilian Weininger
2017 J jnl
Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.
Log. Methods Comput. Sci.
Krishnendu Chatterjee, Zuzana Kretínská, Jan Kretínský
2017 — conf
Value Iteration for Long-Run Average Reward in Markov Decision Processes.
CAV (1)
Pranav Ashok, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretínský, Tobias Meggendorfer
2017 J jnl
Value Iteration for Long-run Average Reward in Markov Decision Processes.
CoRR
Pranav Ashok, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretínský, Tobias Meggendorfer
2016 A conf
Faster Statistical Model Checking for Unbounded Temporal Properties.
TACAS
Przemyslaw Daca, Thomas A. Henzinger, Jan Kretínský, Tatjana Petrov
2016 J jnl
From LTL to deterministic automata - A safraless compositional approach.
Formal Methods Syst. Des.
Javier Esparza, Jan Kretínský, Salomon Sickert
2016 — conf
Limit-Deterministic Büchi Automata for Linear Temporal Logic.
CAV (2)
Salomon Sickert, Javier Esparza, Stefan Jaax, Jan Kretínský
2016 B conf
Linear Distances between Markov Chains.
CONCUR
Przemyslaw Daca, Thomas A. Henzinger, Jan Kretínský, Tatjana Petrov
2016 J jnl
Linear Distances between Markov Chains.
CoRR
Przemyslaw Daca, Thomas A. Henzinger, Jan Kretínský, Tatjana Petrov
2016 B conf
MoChiBA: Probabilistic LTL Model Checking Using Limit-Deterministic Büchi Automata.
ATVA
Salomon Sickert, Jan Kretínský
2016 — conf
Survey of Statistical Verification of Linear Unbounded Properties: Model Checking and Distances.
ISoLA (1)
Jan Kretínský
2015 — conf
Complete Composition Operators for IOCO-Testing Theory.
CBSE
Nikola Benes, Przemyslaw Daca, Thomas A. Henzinger, Jan Kretínský, Dejan Nickovic
2015 B conf
Controller Synthesis for MDPs and Frequency LTL
LPAR
Vojtech Forejt, Jan Krcál, Jan Kretínský
2015 J jnl
Controller synthesis for MDPs and Frequency LTL$\setminus$GU.
CoRR
Vojtech Forejt, Jan Krcál, Jan Kretínský
2015 — conf
Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.
CAV (1)
Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner, Jan Kretínský
2015 J jnl
Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.
CoRR
Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner, Jan Kretínský
2015 J jnl
Faster Statistical Model Checking for Unbounded Temporal Properties.
CoRR
Przemyslaw Daca, Thomas A. Henzinger, Jan Kretínský, Tatjana Petrov
2015 B conf
Polynomial Time Decidability of Weighted Synchronization under Partial Observability.
CONCUR
Jan Kretínský, Kim Guldstrand Larsen, Simon Laursen, Jirí Srba
2015 J jnl
Refinement checking on parametric modal transition systems.
Acta Informatica
Nikola Benes, Jan Kretínský, Kim G. Larsen, Mikael H. Møller, Salomon Sickert, Jirí Srba
2015 — conf
Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games.
HSCC
María Svorenová, Jan Kretínský, Martin Chmelik, Krishnendu Chatterjee, Ivana Cerná, Calin Belta
2015 — conf
The Hanoi Omega-Automata Format.
CAV (1)
Tomás Babiak, Frantisek Blahoudek, Alexandre Duret-Lutz, Joachim Klein, Jan Kretínský, David Müller, David Parker, Jan Strejcek
2015 A* conf
Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.
LICS
Krishnendu Chatterjee, Zuzana Komárková, Jan Kretínský
2015 J jnl
Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.
CoRR
Krishnendu Chatterjee, Zuzana Komárková, Jan Kretínský
2015 — —
Verification of Discrete- and Continuous-Time Non-Deterministic Markovian Systems (Verifikation von non-deterministischen Markovischen Systemen mit diskreter oder kontinuierlicher Zeit)
Jan Kretínský
2014 — conf
Compositionality for Quantitative Specifications.
FACS
Ulrich Fahrenberg, Jan Kretínský, Axel Legay, Louis-Marie Traonouez
2014 J jnl
Compositionality for Quantitative Specifications.
CoRR
Uli Fahrenberg, Jan Kretínský, Axel Legay, Louis-Marie Traonouez
2014 A* conf
From LTL to Deterministic Automata: A Safraless Compositional Approach.
CAV
Javier Esparza, Jan Kretínský
2014 J jnl
From LTL to Deterministic Automata: A Safraless Compositional Approach.
CoRR
Javier Esparza, Jan Kretínský
2014 B conf
Probabilistic Bisimulation: Naturally on Distributions.
CONCUR
Holger Hermanns, Jan Krcál, Jan Kretínský
2014 J jnl
Probabilistic Bisimulation: Naturally on Distributions.
CoRR
Holger Hermanns, Jan Krcál, Jan Kretínský
2014 B conf
Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata.
ATVA
Zuzana Komárková, Jan Kretínský
2014 J jnl
Temporal Logic Control for Stochastic Linear Systems using Abstraction Refinement of Probabilistic Games.
CoRR
María Svorenová, Jan Kretínský, Martin Chmelik, Krishnendu Chatterjee, Ivana Cerná, Calin Belta
2014 B conf
Verification of Markov Decision Processes Using Learning Algorithms.
ATVA
Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Kretínský, Marta Z. Kwiatkowska, David Parker, Mateusz Ujma
2014 J jnl
Verification of Markov Decision Processes using Learning Algorithms.
CoRR
Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Kretínský, Marta Z. Kwiatkowska, David Parker, Mateusz Ujma
2013 J jnl
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
CoRR
Krishnendu Chatterjee, Andreas Gaiser, Jan Kretínský
2013 A* conf
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis.
CAV
Krishnendu Chatterjee, Andreas Gaiser, Jan Kretínský
2013 B conf
Compositional Verification and Optimization of Interactive Markov Chains.
CONCUR
Holger Hermanns, Jan Krcál, Jan Kretínský
2013 J jnl
Compositional Verification and Optimization of Interactive Markov Chains.
CoRR
Holger Hermanns, Jan Krcál, Jan Kretínský
2013 J jnl
Continuous-time stochastic games with time-bounded reachability.
Inf. Comput.
Tomás Brázdil, Vojtech Forejt, Jan Krcál, Jan Kretínský, Antonín Kucera
2013 B conf
Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory.
CONCUR
Nikola Benes, Benoît Delahaye, Uli Fahrenberg, Jan Kretínský, Axel Legay
2013 J jnl
Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory.
CoRR
Nikola Benes, Benoît Delahaye, Uli Fahrenberg, Jan Kretínský, Axel Legay
2013 B conf
MoTraS: A Tool for Modal Transition Systems and Their Extensions.
ATVA
Jan Kretínský, Salomon Sickert
2013 J jnl
On Refinements of Boolean and Parametric Modal Transition Systems
CoRR
Jan Kretínský, Salomon Sickert
2013 C conf
On Refinements of Boolean and Parametric Modal Transition Systems.
ICTAC
Jan Kretínský, Salomon Sickert
2013 B conf
On time-average limits in deterministic and stochastic petri nets.
ICPE
Tomás Brázdil, Lubos Korenciak, Jan Krcál, Jan Kretínský, Vojtech Rehák
2013 B conf
Rabinizer 2: Small Deterministic Automata for LTL ∖ GU.
ATVA
Jan Kretínský, Ruslán Ledesma-Garza
2012 A* conf
Deterministic Automata for the (F, G)-Fragment of LTL.
CAV
Jan Kretínský, Javier Esparza
2012 J jnl
Deterministic Automata for the (F,G)-fragment of LTL
CoRR
Jan Kretínský, Javier Esparza
2012 B conf
Dual-Priced Modal Transition Systems with Time Durations.
LPAR
Nikola Benes, Jan Kretínský, Kim Guldstrand Larsen, Mikael H. Møller, Jirí Srba
2012 J jnl
EXPTIME-completeness of thorough refinement on modal transition systems.
Inf. Comput.
Nikola Benes, Jan Kretínský, Kim G. Larsen, Jirí Srba
2012 C conf
Modal Process Rewrite Systems.
ICTAC
Nikola Benes, Jan Kretínský
2012 B conf
Rabinizer: Small Deterministic Automata for LTL(F, G).
ATVA
Andreas Gaiser, Jan Kretínský, Javier Esparza
2012 — conf
Verification of Open Interactive Markov Chains.
FSTTCS
Tomás Brázdil, Holger Hermanns, Jan Krcál, Jan Kretínský, Vojtech Rehák
2011 B conf
Fixed-Delay Events in Generalized Semi-Markov Processes Revisited.
CONCUR
Tomás Brázdil, Jan Krcál, Jan Kretínský, Vojtech Rehák
2011 J jnl
Fixed-delay Events in Generalized Semi-Markov Processes Revisited
CoRR
Tomás Brázdil, Jan Krcál, Jan Kretínský, Vojtech Rehák
2011 J jnl
Measuring Performance of Continuous-Time Stochastic Processes using Timed Automata
CoRR
Tomás Brázdil, Jan Krcál, Jan Kretínský, Antonín Kucera, Vojtech Rehák
2011 — conf
Measuring performance of continuous-time stochastic processes using timed automata.
HSCC
Tomás Brázdil, Jan Krcál, Jan Kretínský, Antonín Kucera, Vojtech Rehák
2011 B conf
Modal Transition Systems: Composition and LTL Model Checking.
ATVA
Nikola Benes, Ivana Cerná, Jan Kretínský
2011 B conf
Parametric Modal Transition Systems.
ATVA
Nikola Benes, Jan Kretínský, Kim G. Larsen, Mikael H. Møller, Jirí Srba
2010 — conf
Process Algebra for Modal Transition Systemses.
MEMICS
Nikola Benes, Jan Kretínský
2010 B conf
Stochastic Real-Time Games with Qualitative Timed Automata Objectives.
CONCUR
Tomás Brázdil, Jan Krcál, Jan Kretínský, Antonín Kucera, Vojtech Rehák
2009 C conf
Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete.
ICTAC
Nikola Benes, Jan Kretínský, Kim Guldstrand Larsen, Jirí Srba
2009 — conf
Continuous-Time Stochastic Games with Time-Bounded Reachability.
FSTTCS
Tomás Brázdil, Vojtech Forejt, Jan Krcál, Jan Kretínský, Antonín Kucera
2009 J jnl
On determinism in modal transition systems.
Theor. Comput. Sci.
Nikola Benes, Jan Kretínský, Kim Guldstrand Larsen, Jirí Srba
2008 A* conf
The Satisfiability Problem for Probabilistic CTL.
LICS
Tomás Brázdil, Vojtech Forejt, Jan Kretínský, Antonín Kucera