![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
Jan Kretínský
Person information
- unicode name: Jan Křetínský
- affiliation: Masaryk University, Brno, Czech Republic
- affiliation: Technical University of Munich, Department of Informatics, Germany
Refine list
![note](https://dblp.uni-trier.de/img/note-mark.dark.12x12.png)
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Books and Theses
- 2015
- [b1]Jan Kretínský:
Verification of Discrete- and Continuous-Time Non-Deterministic Markovian Systems (Verifikation von non-deterministischen Markovischen Systemen mit diskreter oder kontinuierlicher Zeit). Technical University of Munich, Germany, 2015
Journal Articles
- 2023
- [j17]Florian Jüngermann, Jan Kretínský, Maximilian Weininger
:
Algebraically explainable controllers: decision trees and support vector machines join forces. Int. J. Softw. Tools Technol. Transf. 25(3): 249-266 (2023) - 2022
- [j16]Jan Kretínský
, Tobias Meggendorfer
, Clara Waldmann
, Maximilian Weininger
:
Index appearance record with preorders. Acta Informatica 59(5): 585-618 (2022) - [j15]Julia Eisentraut
, Edon Kelmendi
, Jan Kretínský, Maximilian Weininger
:
Value iteration for simple stochastic games: Stopping criterion and learning algorithm. Inf. Comput. 285(Part): 104886 (2022) - [j14]Jan Kretínský, Emanuel Ramneantu, Alexander Slivinskiy, Maximilian Weininger
:
Comparison of algorithms for simple stochastic games. Inf. Comput. 289(Part): 104885 (2022) - [j13]Javier Esparza, Jan Kretínský, Jean-François Raskin, Salomon Sickert:
From linear temporal logic and limit-deterministic Büchi automata to deterministic parity automata. Int. J. Softw. Tools Technol. Transf. 24(4): 635-659 (2022) - 2021
- [j12]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:
Formalizing and guaranteeing human-robot interaction. Commun. ACM 64(9): 78-84 (2021) - 2020
- [j11]Nikola Benes
, Uli Fahrenberg, Jan Kretínský, Axel Legay, Louis-Marie Traonouez:
Logical vs. behavioural specifications. Inf. Comput. 271: 104487 (2020) - [j10]Javier Esparza
, Jan Kretínský, Salomon Sickert:
A Unified Translation of Linear Temporal Logic to ω-Automata. J. ACM 67(6): 33:1-33:61 (2020) - [j9]Jan Kretínský, Tobias Meggendorfer:
Of Cores: A Partial-Exploration Framework for Markov Decision Processes. Log. Methods Comput. Sci. 16(4) (2020) - 2018
- [j8]Uli Fahrenberg
, Jan Kretínský, Axel Legay, Louis-Marie Traonouez:
Compositionality for quantitative specifications. Soft Comput. 22(4): 1139-1158 (2018) - 2017
- [j7]Krishnendu Chatterjee
, Zuzana Kretínská, Jan Kretínský:
Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. Log. Methods Comput. Sci. 13(2) (2017) - [j6]Przemyslaw Daca, Thomas A. Henzinger, Jan Kretínský, Tatjana Petrov
:
Faster Statistical Model Checking for Unbounded Temporal Properties. ACM Trans. Comput. Log. 18(2): 12:1-12:25 (2017) - 2016
- [j5]Javier Esparza
, Jan Kretínský
, Salomon Sickert
:
From LTL to deterministic automata - A safraless compositional approach. Formal Methods Syst. Des. 49(3): 219-271 (2016) - 2015
- [j4]Nikola Benes
, Jan Kretínský, Kim G. Larsen
, Mikael H. Møller, Salomon Sickert, Jirí Srba
:
Refinement checking on parametric modal transition systems. Acta Informatica 52(2-3): 269-297 (2015) - 2013
- [j3]Tomás Brázdil, Vojtech Forejt, Jan Krcál, Jan Kretínský, Antonín Kucera
:
Continuous-time stochastic games with time-bounded reachability. Inf. Comput. 224: 46-70 (2013) - 2012
- [j2]Nikola Benes
, Jan Kretínský, Kim G. Larsen
, Jirí Srba
:
EXPTIME-completeness of thorough refinement on modal transition systems. Inf. Comput. 218: 54-68 (2012) - 2009
- [j1]Nikola Benes
, Jan Kretínský, Kim Guldstrand Larsen
, Jirí Srba
:
On determinism in modal transition systems. Theor. Comput. Sci. 410(41): 4026-4043 (2009)
Conference and Workshop Papers
- 2024
- [c97]Muqsit Azeem
, Marta Grobelna
, Sudeep Kanav
, Jan Kretínský
, Stefanie Mohr
, Sabine Rieder
:
Monitizer: Automating Design and Evaluation of Neural Network Monitors. CAV (2) 2024: 265-279 - [c96]Severin Bals
, Alexandros Evangelidis
, Jan Kretínský
, Jakob Waibel
:
MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints✱. HSCC 2024: 24:1-24:7 - [c95]Severin Bals
, Alexandros Evangelidis
, Jan Kretínský
, Jakob Waibel
:
Poster Abstract: MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints✱. HSCC 2024: 33:1-33:2 - [c94]Alexander Bork
, Debraj Chakraborty
, Kush Grover
, Jan Kretínský
, Stefanie Mohr
:
Learning Explainable and Better Performing Representations of POMDP Strategies. TACAS (2) 2024: 299-319 - 2023
- [c93]Calvin Chau
, Jan Kretínský
, Stefanie Mohr
:
Syntactic vs Semantic Linear Abstraction and Refinement of Neural Networks. ATVA (1) 2023: 401-421 - [c92]Jan Kretínský
, Tobias Meggendorfer
, Maximilian Prokop
, Sabine Rieder
:
Guessing Winning Policies in LTL Synthesis by Semantic Learning. CAV (1) 2023: 390-414 - [c91]Vahid Hashemi, Jan Kretínský, Sabine Rieder
, Jessica Schmidt:
Runtime Monitoring for Out-of-Distribution Detection in Object Detection Neural Networks. FM 2023: 622-634 - [c90]Florian Dorfhuber, Julia Eisentraut, Jan Kretínský:
Learning Attack Trees by Genetic Algorithms. ICTAC 2023: 55-73 - [c89]Jan Kretínský, Tobias Meggendorfer, Maximilian Weininger
:
Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives. LICS 2023: 1-14 - [c88]Nils Jansen
, Bettina Könighofer, Jan Kretínský, Kim G. Larsen:
Welcome Remarks from AISoLA 2023/Track C2 Chairs. AISoLA 2023: 25-32 - 2022
- [c87]Muqsit Azeem
, Alexandros Evangelidis
, Jan Kretínský
, Alexander Slivinskiy
, Maximilian Weininger
:
Optimistic and Topological Value Iteration for Simple Stochastic Games. ATVA 2022: 285-302 - [c86]Miroslav Chodil
, Antonín Kucera
, Jan Kretínský
:
Satisfiability of Quantitative Probabilistic CTL: Rise to the Challenge. Principles of Systems Design 2022: 364-387 - [c85]Chaitanya Agarwal, Shibashis Guha, Jan Kretínský, Pazhamalai Muruganandham:
PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP. CAV (2) 2022: 3-25 - [c84]Martin Helfrich
, Milan Ceska
, Jan Kretínský
, Stefan Marticek
:
Abstraction-Based Segmental Simulation of Chemical Reaction Networks. CMSB 2022: 41-60 - [c83]Kush Grover
, Jan Kretínský, Tobias Meggendorfer, Maximilian Weininger
:
Anytime Guarantees for Reachability in Uncountable Markov Decision Processes. CONCUR 2022: 11:1-11:20 - [c82]Jonis Kiesbye, Kush Grover
, Pranav Ashok, Jan Kretínský:
Planning via model checking with decision-tree controllers. ICRA 2022: 4347-4354 - [c81]Luca Bortolussi
, Giuseppe Maria Gallo, Jan Kretínský
, Laura Nenzi
:
Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes. TACAS (1) 2022: 281-300 - 2021
- [c80]Maximilian Weininger
, Kush Grover
, Shruti Misra, Jan Kretínský:
Guaranteed Trade-Offs in Dynamic Information Flow Tracking Games. CDC 2021: 3786-3793 - [c79]Javier Esparza, Stefan Kiefer, Jan Kretínský, Maximilian Weininger
:
Enforcing ω-Regular Properties in Markov Chains by Restarting. CONCUR 2021: 5:1-5:22 - [c78]Julia Eisentraut
, Stephan Holzer, Katharina Klioba, Jan Kretínský, Lukas Pin, Alexander Wagner:
Assessing Security of Cryptocurrencies with Attack-Defense Trees: Proof of Concept and Future Directions. ICTAC 2021: 214-234 - [c77]Jan Kretínský:
LTL-Constrained Steady-State Policy Synthesis. IJCAI 2021: 4104-4111 - [c76]Kush Grover
, Fernando S. Barbosa, Jana Tumova, Jan Kretínský:
Semantic Abstraction-Guided Motion Planning for scLTL Missions in Unknown Environments. Robotics: Science and Systems 2021 - [c75]Vahid Hashemi
, Jan Kretínský
, Stefanie Mohr
, Emmanouil Seferis:
Gaussian-Based Runtime Detection of Out-of-distribution Inputs for Neural Networks. RV 2021: 254-264 - [c74]Pranav Ashok
, Mathias Jackermeier
, Jan Kretínský
, Christoph Weinhuber
, Maximilian Weininger
, Mayank Yadav
:
dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts. TACAS (2) 2021: 326-345 - 2020
- [c73]Pranav Ashok
, Vahid Hashemi
, Jan Kretínský
, Stefanie Mohr
:
DeepAbstract: Neural Network Abstraction for Accelerating Verification. ATVA 2020: 92-107 - [c72]Loris D'Antoni, Martin Helfrich
, Jan Kretínský, Emanuel Ramneantu, Maximilian Weininger
:
Automata Tutor v3. CAV (2) 2020: 3-14 - [c71]Milan Ceska
, Calvin Chau
, Jan Kretínský:
SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks. CAV (1) 2020: 653-666 - [c70]Pranav Ashok
, Mathias Jackermeier, Pushpak Jagtap
, Jan Kretínský, Maximilian Weininger
, Majid Zamani:
dtControl: decision tree learning algorithms for controller representation. HSCC 2020: 17:1-17:7 - [c69]Pranav Ashok, Mathias Jackermeier
, Pushpak Jagtap
, Jan Kretínský, Maximilian Weininger
, Majid Zamani:
dtControl: decision tree learning algorithms for controller representation. HSCC 2020: 30:1-30:2 - [c68]Carlos E. Budde
, Arnd Hartmanns
, Michaela Klauck
, Jan Kretínský
, David Parker
, Tim Quatmann
, Andrea Turrini
, Zhen Zhang
:
On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report. ISoLA (4) 2020: 216-241 - [c67]Pranav Ashok, Przemyslaw Daca, Jan Kretínský, Maximilian Weininger
:
Statistical Model Checking: Black or White? ISoLA (1) 2020: 331-349 - [c66]Pranav Ashok
, Krishnendu Chatterjee, Jan Kretínský, Maximilian Weininger
, Tobias Winkler
:
Approximating Values of Generalized-Reachability Stochastic Games. LICS 2020: 102-115 - [c65]Jan Kretínský, Fabian Michel, Lukas Michel, Guillermo A. Pérez:
Finite-Memory Near-Optimal Learning for Markov Decision Processes with Long-Run Average Reward. UAI 2020: 1149-1158 - [c64]Jan Kretínský, Emanuel Ramneantu, Alexander Slivinskiy, Maximilian Weininger
:
Comparison of Algorithms for Simple Stochastic Games. GandALF 2020: 131-148 - 2019
- [c63]Jan Kretínský
, Alexander Manta
, Tobias Meggendorfer
:
Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis. ATVA 2019: 404-422 - [c62]Milan Ceska
, Jan Kretínský:
Semi-quantitative Abstraction and Analysis of Chemical Reaction Networks. CAV (1) 2019: 475-496 - [c61]Pranav Ashok
, Jan Kretínský, Maximilian Weininger
:
PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games. CAV (1) 2019: 497-519 - [c60]Maximilian Weininger
, Tobias Meggendorfer
, Jan Kretínský:
Satisfiability Bounds for ω-Regular Properties in Bounded-Parameter Markov Decision Processes. CDC 2019: 2284-2291 - [c59]Milan Ceska
, Jan Kretínský:
Semi-quantitative Abstraction and Analysis of Chemical Reaction Networks (Extended Abstract). CMSB 2019: 337-341 - [c58]Jan Kretínský, Tobias Meggendorfer
:
Of Cores: A Partial-Exploration Framework for Markov Decision Processes. CONCUR 2019: 5:1-5:17 - [c57]Pranav Ashok
, Tomás Brázdil, Krishnendu Chatterjee, Jan Kretínský, Christoph H. Lampert, Viktor Toman
:
Strategy Representation by Decision Trees with Linear Classifiers. QEST 2019: 109-128 - [c56]Pranav Ashok
, Jan Kretínský, Kim Guldstrand Larsen
, Adrien Le Coënt, Jakob Haahr Taankvist, Maximilian Weininger
:
SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processes. QEST 2019: 147-164 - [c55]Julia Eisentraut
, Jan Kretínský:
Expected Cost Analysis of Attack-Defense Trees. QEST 2019: 203-221 - [c54]Ernst Moritz Hahn
, Arnd Hartmanns
, Christian Hensel, Michaela Klauck, Joachim Klein
, Jan Kretínský
, David Parker
, Tim Quatmann
, Enno Ruijters
, Marcel Steinmetz:
The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report). TACAS (3) 2019: 69-92 - 2018
- [c53]Pranav Ashok
, Yuliya Butkova
, Holger Hermanns
, Jan Kretínský
:
Continuous-Time Markov Decisions Based on Partial Exploration. ATVA 2018: 317-334 - [c52]Jan Kretínský
, Tobias Meggendorfer
, Salomon Sickert
:
Owl: A Library for ω-Words, Automata, and LTL. ATVA 2018: 543-550 - [c51]Jan Kretínský, Tobias Meggendorfer
, Salomon Sickert
, Christopher Ziegler:
Rabinizer 4: From LTL to Your Favourite Deterministic Automaton. CAV (1) 2018: 567-577 - [c50]Edon Kelmendi, Julia Krämer, Jan Kretínský, Maximilian Weininger
:
Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm. CAV (1) 2018: 623-642 - [c49]Jan Kretínský, Guillermo A. Pérez
, Jean-François Raskin:
Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints. CONCUR 2018: 8:1-8:18 - [c48]Jan Kretínský, Alexej Rotar:
The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL. CONCUR 2018: 32:1-32:16 - [c47]Pranav Ashok
, Tomás Brázdil, Jan Kretínský, Ondrej Slámecka:
Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes. ISoLA (2) 2018: 322-335 - [c46]Javier Esparza
, Jan Kretínský, Salomon Sickert:
One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata. LICS 2018: 384-393 - [c45]Jan Kretínský, Tobias Meggendorfer
:
Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes. LICS 2018: 609-618 - [c44]Tomás Brázdil, Krishnendu Chatterjee, Jan Kretínský
, Viktor Toman
:
Strategy Representation by Decision Trees in Reactive Synthesis. TACAS (1) 2018: 385-407 - 2017
- [c43]Jan Kretínský, Tobias Meggendorfer
:
Efficient Strategy Iteration for Mean Payoff in Markov Decision Processes. ATVA 2017: 380-399 - [c42]Jan Kretínský:
30 Years of Modal Transition Systems: Survey of Extensions and Analysis. Models, Algorithms, Logics and Tools 2017: 36-74 - [c41]Pranav Ashok
, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretínský, Tobias Meggendorfer
:
Value Iteration for Long-Run Average Reward in Markov Decision Processes. CAV (1) 2017: 201-221 - [c40]Javier Esparza
, Jan Kretínský, Jean-François Raskin
, Salomon Sickert:
From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata. TACAS (1) 2017: 426-442 - [c39]Jan Kretínský, Tobias Meggendorfer
, Clara Waldmann
, Maximilian Weininger
:
Index Appearance Record for Transforming Rabin Automata into Parity Automata. TACAS (1) 2017: 443-460 - 2016
- [c38]Salomon Sickert
, Jan Kretínský:
MoChiBA: Probabilistic LTL Model Checking Using Limit-Deterministic Büchi Automata. ATVA 2016: 130-137 - [c37]Salomon Sickert
, Javier Esparza
, Stefan Jaax, Jan Kretínský:
Limit-Deterministic Büchi Automata for Linear Temporal Logic. CAV (2) 2016: 312-332 - [c36]Przemyslaw Daca, Thomas A. Henzinger, Jan Kretínský, Tatjana Petrov
:
Linear Distances between Markov Chains. CONCUR 2016: 20:1-20:15 - [c35]Jan Kretínský:
Survey of Statistical Verification of Linear Unbounded Properties: Model Checking and Distances. ISoLA (1) 2016: 27-45 - [c34]Przemyslaw Daca, Thomas A. Henzinger, Jan Kretínský, Tatjana Petrov
:
Faster Statistical Model Checking for Unbounded Temporal Properties. TACAS 2016: 112-129 - 2015
- [c33]Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner, Jan Kretínský:
Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. CAV (1) 2015: 158-177 - [c32]Tomás Babiak, Frantisek Blahoudek
, Alexandre Duret-Lutz
, Joachim Klein
, Jan Kretínský, David Müller, David Parker
, Jan Strejcek
:
The Hanoi Omega-Automata Format. CAV (1) 2015: 479-486 - [c31]Nikola Benes
, Przemyslaw Daca, Thomas A. Henzinger, Jan Kretínský, Dejan Nickovic:
Complete Composition Operators for IOCO-Testing Theory. CBSE 2015: 101-110 - [c30]Jan Kretínský, Kim Guldstrand Larsen
, Simon Laursen
, Jirí Srba
:
Polynomial Time Decidability of Weighted Synchronization under Partial Observability. CONCUR 2015: 142-154 - [c29]María Svorenová, Jan Kretínský, Martin Chmelik, Krishnendu Chatterjee, Ivana Cerná
, Calin Belta:
Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. HSCC 2015: 259-268 - [c28]Krishnendu Chatterjee, Zuzana Komárková, Jan Kretínský:
Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. LICS 2015: 244-256 - [c27]Vojtech Forejt, Jan Krcál, Jan Kretínský:
Controller Synthesis for MDPs and Frequency LTL\GU. LPAR 2015: 162-177 - 2014
- [c26]Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Kretínský, Marta Z. Kwiatkowska, David Parker
, Mateusz Ujma:
Verification of Markov Decision Processes Using Learning Algorithms. ATVA 2014: 98-114 - [c25]Zuzana Komárková, Jan Kretínský:
Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata. ATVA 2014: 235-241 - [c24]Javier Esparza
, Jan Kretínský:
From LTL to Deterministic Automata: A Safraless Compositional Approach. CAV 2014: 192-208 - [c23]Holger Hermanns, Jan Krcál, Jan Kretínský:
Probabilistic Bisimulation: Naturally on Distributions. CONCUR 2014: 249-265 - [c22]Ulrich Fahrenberg, Jan Kretínský, Axel Legay, Louis-Marie Traonouez:
Compositionality for Quantitative Specifications. FACS 2014: 306-324 - 2013
- [c21]Jan Kretínský, Ruslán Ledesma-Garza:
Rabinizer 2: Small Deterministic Automata for LTL ∖ GU. ATVA 2013: 446-450 - [c20]Jan Kretínský, Salomon Sickert:
MoTraS: A Tool for Modal Transition Systems and Their Extensions. ATVA 2013: 487-491 - [c19]Krishnendu Chatterjee, Andreas Gaiser, Jan Kretínský:
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. CAV 2013: 559-575 - [c18]Nikola Benes
, Benoît Delahaye
, Uli Fahrenberg, Jan Kretínský, Axel Legay:
Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory. CONCUR 2013: 76-90 - [c17]Holger Hermanns, Jan Krcál, Jan Kretínský:
Compositional Verification and Optimization of Interactive Markov Chains. CONCUR 2013: 364-379 - [c16]Jan Kretínský, Salomon Sickert
:
On Refinements of Boolean and Parametric Modal Transition Systems. ICTAC 2013: 213-230 - [c15]Tomás Brázdil, Lubos Korenciak, Jan Krcál, Jan Kretínský, Vojtech Rehák
:
On time-average limits in deterministic and stochastic petri nets. ICPE 2013: 421-422 - 2012
- [c14]Andreas Gaiser, Jan Kretínský, Javier Esparza
:
Rabinizer: Small Deterministic Automata for LTL(F, G). ATVA 2012: 72-76 - [c13]Jan Kretínský, Javier Esparza
:
Deterministic Automata for the (F, G)-Fragment of LTL. CAV 2012: 7-22 - [c12]Tomás Brázdil, Holger Hermanns
, Jan Krcál, Jan Kretínský, Vojtech Rehák
:
Verification of Open Interactive Markov Chains. FSTTCS 2012: 474-485 - [c11]Nikola Benes
, Jan Kretínský:
Modal Process Rewrite Systems. ICTAC 2012: 120-135 - [c10]Nikola Benes
, Jan Kretínský, Kim Guldstrand Larsen
, Mikael H. Møller, Jirí Srba
:
Dual-Priced Modal Transition Systems with Time Durations. LPAR 2012: 122-137 - 2011
- [c9]Nikola Benes
, Ivana Cerná
, Jan Kretínský:
Modal Transition Systems: Composition and LTL Model Checking. ATVA 2011: 228-242 - [c8]Nikola Benes
, Jan Kretínský, Kim G. Larsen
, Mikael H. Møller, Jirí Srba
:
Parametric Modal Transition Systems. ATVA 2011: 275-289 - [c7]Tomás Brázdil, Jan Krcál, Jan Kretínský, Vojtech Rehák:
Fixed-Delay Events in Generalized Semi-Markov Processes Revisited. CONCUR 2011: 140-155 - [c6]Tomás Brázdil, Jan Krcál, Jan Kretínský, Antonín Kucera, Vojtech Rehák:
Measuring performance of continuous-time stochastic processes using timed automata. HSCC 2011: 33-42 - 2010
- [c5]Tomás Brázdil, Jan Krcál, Jan Kretínský, Antonín Kucera, Vojtech Rehák:
Stochastic Real-Time Games with Qualitative Timed Automata Objectives. CONCUR 2010: 207-221 - [c4]Nikola Benes
, Jan Kretínský:
Process Algebra for Modal Transition Systemses. MEMICS 2010: 9-18 - 2009
- [c3]Tomás Brázdil, Vojtech Forejt, Jan Krcál, Jan Kretínský, Antonín Kucera:
Continuous-Time Stochastic Games with Time-Bounded Reachability. FSTTCS 2009: 61-72 - [c2]Nikola Benes
, Jan Kretínský, Kim Guldstrand Larsen
, Jirí Srba
:
Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete. ICTAC 2009: 112-126 - 2008
- [c1]Tomás Brázdil, Vojtech Forejt, Jan Kretínský, Antonín Kucera
:
The Satisfiability Problem for Probabilistic CTL. LICS 2008: 391-402
Editorship
- 2024
- [e1]Stefan Kiefer, Jan Kretínský, Antonín Kucera:
Taming the Infinities of Concurrency - Essays Dedicated to Javier Esparza on the Occasion of His 60th Birthday. Lecture Notes in Computer Science 14660, Springer 2024, ISBN 978-3-031-56221-1 [contents]
Informal and Other Publications
- 2024
- [i65]Alexander Bork, Debraj Chakraborty, Kush Grover
, Jan Kretínský, Stefanie Mohr:
Learning Explainable and Better Performing Representations of POMDP Strategies. CoRR abs/2401.07656 (2024) - [i64]Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Kretínský, Marta Kwiatkowska, Tobias Meggendorfer, David Parker, Mateusz Ujma:
Learning Algorithms for Verification of Markov Decision Processes. CoRR abs/2403.09184 (2024) - [i63]Muqsit Azeem, Marta Grobelna, Sudeep Kanav, Jan Kretínský, Stefanie Mohr, Sabine Rieder:
Monitizer: Automating Design and Evaluation of Neural Network Monitors. CoRR abs/2405.10350 (2024) - [i62]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:
Tools at the Frontiers of Quantitative Verification. CoRR abs/2405.13583 (2024) - [i61]Gaia Saveri, Laura Nenzi, Luca Bortolussi, Jan Kretínský:
stl2vec: Semantic and Interpretable Vector Representation of Temporal Logic. CoRR abs/2405.14389 (2024) - [i60]Florian Dorfhuber, Julia Eisentraut, Katharina Klioba, Jan Kretínský:
QuADTool: Attack-Defense-Tree Synthesis, Analysis and Bridge to Verification. CoRR abs/2406.15605 (2024) - 2023
- [i59]Jan Kretínský, Tobias Meggendorfer, Maximilian Weininger
:
Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives. CoRR abs/2304.09930 (2023) - [i58]Jan Kretínský, Tobias Meggendorfer, Maximilian Prokop, Sabine Rieder:
Guessing Winning Policies in LTL Synthesis by Semantic Learning. CoRR abs/2305.15109 (2023) - [i57]Severin Bals, Alexandros Evangelidis, Kush Grover, Jan Kretínský, Jakob Waibel:
MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints. CoRR abs/2305.16752 (2023) - [i56]Calvin Chau, Jan Kretínský, Stefanie Mohr:
Syntactic vs Semantic Linear Abstraction and Refinement of Neural Networks. CoRR abs/2307.10891 (2023) - 2022
- [i55]Luca Bortolussi, Giuseppe Maria Gallo, Jan Kretínský, Laura Nenzi:
Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes. CoRR abs/2201.09928 (2022) - [i54]Chaitanya Agarwal, Shibashis Guha, Jan Kretínský, M. Pazhamalai:
PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP. CoRR abs/2206.01465 (2022) - [i53]Martin Helfrich, Milan Ceska
, Jan Kretínský, Stefan Marticek:
Abstraction-Based Segmental Simulation of Chemical Reaction Networks. CoRR abs/2206.06677 (2022) - [i52]Jan Kretínský, Tobias Meggendorfer, Maximilian Weininger
:
Satisfiability Bounds for ω-Regular Properties in Bounded-Parameter Markov Decision Processes. CoRR abs/2207.13660 (2022) - [i51]Muqsit Azeem, Alexandros Evangelidis
, Jan Kretínský, Alexander Slivinskiy, Maximilian Weininger
:
Optimistic and Topological Value Iteration for Simple Stochastic Games. CoRR abs/2207.14417 (2022) - [i50]Florian Jüngermann, Jan Kretínský, Maximilian Weininger
:
Algebraically Explainable Controllers: Decision Trees and Support Vector Machines Join Forces. CoRR abs/2208.12804 (2022) - [i49]Vahid Hashemi, Jan Kretínský, Sabine Rieder, Jessica Schmidt:
Runtime Monitoring for Out-of-Distribution Detection in Object Detection Neural Networks. CoRR abs/2212.07773 (2022) - 2021
- [i48]Pranav Ashok, Mathias Jackermeier, Jan Kretínský, Christoph Weinhuber, Maximilian Weininger, Mayank Yadav:
dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts. CoRR abs/2101.07202 (2021) - [i47]Jan Kretínský:
LTL-Constrained Steady-State Policy Synthesis. CoRR abs/2105.14894 (2021) - 2020
- [i46]Pranav Ashok, Mathias Jackermeier, Pushpak Jagtap, Jan Kretínský, Maximilian Weininger, Majid Zamani:
dtControl: Decision Tree Learning Algorithms for Controller Representation. CoRR abs/2002.04991 (2020) - [i45]Loris D'Antoni, Martin Helfrich, Jan Kretínský, Emanuel Ramneantu, Maximilian Weininger:
Automata Tutor v3. CoRR abs/2005.01419 (2020) - [i44]Pranav Ashok
, Vahid Hashemi, Jan Kretínský, Stefanie Mohr:
DeepAbstract: Neural Network Abstraction for Accelerating Verification. CoRR abs/2006.13735 (2020) - [i43]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:
Formalizing and Guaranteeing* Human-Robot Interaction. CoRR abs/2006.16732 (2020) - [i42]Kush Grover, Jan Kretínský, Tobias Meggendorfer, Maximilian Weininger:
An Anytime Algorithm for Reachability on Uncountable MDP. CoRR abs/2008.04824 (2020) - [i41]Jan Kretínský, Emanuel Ramneantu, Alexander Slivinskiy, Maximilian Weininger:
Comparison of Algorithms for Simple Stochastic Games (Full Version). CoRR abs/2008.09465 (2020) - [i40]Javier Esparza, Stefan Kiefer, Jan Kretínský, Maximilian Weininger:
Online Monitoring ω-Regular Properties in Unknown Markov Chains. CoRR abs/2010.08347 (2020) - 2019
- [i39]Pranav Ashok, Jan Kretínský, Maximilian Weininger:
PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games. CoRR abs/1905.04403 (2019) - [i38]Milan Ceska, Jan Kretínský:
Semi-Quantitative Abstraction and Analysis of Chemical Reaction Networks. CoRR abs/1905.09914 (2019) - [i37]Jan Kretínský, Tobias Meggendorfer:
Of Cores: A Partial-Exploration Framework for Markov Decision Processes. CoRR abs/1906.06931 (2019) - [i36]Pranav Ashok, Tomás Brázdil, Krishnendu Chatterjee, Jan Kretínský, Christoph H. Lampert, Viktor Toman:
Strategy Representation by Decision Trees with Linear Classifiers. CoRR abs/1906.08178 (2019) - [i35]Pranav Ashok, Jan Kretínský, Kim Guldstrand Larsen, Adrien Le Coënt, Jakob Haahr Taankvist, Maximilian Weininger:
SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processes. CoRR abs/1906.10640 (2019) - [i34]Jan Kretínský, Alexander Manta, Tobias Meggendorfer:
Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis. CoRR abs/1907.12157 (2019) - [i33]Pranav Ashok
, Jan Kretínský, Maximilian Weininger:
Approximating Values of Generalized-Reachability Stochastic Games. CoRR abs/1908.05106 (2019) - [i32]Julia Eisentraut, Jan Kretínský, Alexej Rotar:
Stopping Criteria for Value and Strategy Iteration on Concurrent Stochastic Reachability Games. CoRR abs/1909.08348 (2019) - 2018
- [i31]Tomás Brázdil, Krishnendu Chatterjee, Jan Kretínský, Viktor Toman:
Strategy Representation by Decision Trees in Reactive Synthesis. CoRR abs/1802.00758 (2018) - [i30]Edon Kelmendi, Julia Krämer, Jan Kretínský, Maximilian Weininger:
Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm. CoRR abs/1804.04901 (2018) - [i29]Jan Kretínský, Guillermo A. Pérez, Jean-François Raskin:
Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints. CoRR abs/1804.08924 (2018) - [i28]Javier Esparza, Jan Kretínský, Salomon Sickert:
One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata. CoRR abs/1805.00748 (2018) - [i27]Jan Kretínský, Tobias Meggendorfer:
Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes. CoRR abs/1805.02946 (2018) - [i26]Jan Kretínský, Alexej Rotar:
The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL. CoRR abs/1806.11418 (2018) - [i25]Jan Kretínský, Tobias Meggendorfer, Salomon Sickert:
LTL Store: Repository of LTL formulae from literature and case studies. CoRR abs/1807.03296 (2018) - [i24]Pranav Ashok, Yuliya Butkova, Holger Hermanns, Jan Kretínský:
Continuous-Time Markov Decisions based on Partial Exploration. CoRR abs/1807.09641 (2018) - [i23]Pranav Ashok, Tomás Brázdil, Jan Kretínský, Ondrej Slámecka:
Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes. CoRR abs/1809.03299 (2018) - [i22]Nils Jansen
, Joost-Pieter Katoen, Pushmeet Kohli, Jan Kretínský:
Machine Learning and Model Checking Join Forces (Dagstuhl Seminar 18121). Dagstuhl Reports 8(3): 74-93 (2018) - 2017
- [i21]Jan Kretínský, Tobias Meggendorfer, Clara Waldmann
, Maximilian Weininger:
Index appearance record for transforming Rabin automata into parity automata. CoRR abs/1701.05738 (2017) - [i20]Javier Esparza, Jan Kretínský, Jean-François Raskin, Salomon Sickert:
From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata. CoRR abs/1701.06103 (2017) - [i19]Pranav Ashok, Krishnendu Chatterjee, Przemyslaw Daca, Jan Kretínský, Tobias Meggendorfer:
Value Iteration for Long-run Average Reward in Markov Decision Processes. CoRR abs/1705.02326 (2017) - [i18]Jan Kretínský, Tobias Meggendorfer:
Efficient Strategy Iteration for Mean Payoff in Markov Decision Processes. CoRR abs/1707.01859 (2017) - 2016
- [i17]Przemyslaw Daca, Thomas A. Henzinger, Jan Kretínský, Tatjana Petrov:
Linear Distances between Markov Chains. CoRR abs/1605.00186 (2016) - 2015
- [i16]Krishnendu Chatterjee, Zuzana Komárková, Jan Kretínský:
Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. CoRR abs/1502.00611 (2015) - [i15]Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner, Jan Kretínský:
Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. CoRR abs/1502.02834 (2015) - [i14]Przemyslaw Daca, Thomas A. Henzinger, Jan Kretínský, Tatjana Petrov:
Faster Statistical Model Checking for Unbounded Temporal Properties. CoRR abs/1504.05739 (2015) - [i13]Vojtech Forejt, Jan Krcál, Jan Kretínský:
Controller synthesis for MDPs and Frequency LTL$\setminus$GU. CoRR abs/1509.04116 (2015) - 2014
- [i12]Tomás Brázdil, Krishnendu Chatterjee, Martin Chmelik, Vojtech Forejt, Jan Kretínský, Marta Z. Kwiatkowska, David Parker, Mateusz Ujma:
Verification of Markov Decision Processes using Learning Algorithms. CoRR abs/1402.2967 (2014) - [i11]Javier Esparza, Jan Kretínský:
From LTL to Deterministic Automata: A Safraless Compositional Approach. CoRR abs/1402.3388 (2014) - [i10]Holger Hermanns, Jan Krcál, Jan Kretínský:
Probabilistic Bisimulation: Naturally on Distributions. CoRR abs/1404.5084 (2014) - [i9]Uli Fahrenberg, Jan Kretínský, Axel Legay, Louis-Marie Traonouez:
Compositionality for Quantitative Specifications. CoRR abs/1408.1256 (2014) - [i8]María Svorenová, Jan Kretínský, Martin Chmelik, Krishnendu Chatterjee, Ivana Cerná, Calin Belta:
Temporal Logic Control for Stochastic Linear Systems using Abstraction Refinement of Probabilistic Games. CoRR abs/1410.5387 (2014) - 2013
- [i7]Jan Kretínský, Salomon Sickert:
On Refinements of Boolean and Parametric Modal Transition Systems. CoRR abs/1304.5278 (2013) - [i6]Krishnendu Chatterjee, Andreas Gaiser, Jan Kretínský:
Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. CoRR abs/1304.5281 (2013) - [i5]Holger Hermanns, Jan Krcál, Jan Kretínský:
Compositional Verification and Optimization of Interactive Markov Chains. CoRR abs/1305.7332 (2013) - [i4]Nikola Benes, Benoît Delahaye, Uli Fahrenberg, Jan Kretínský, Axel Legay:
Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory. CoRR abs/1306.0741 (2013) - 2012
- [i3]Jan Kretínský, Javier Esparza:
Deterministic Automata for the (F,G)-fragment of LTL. CoRR abs/1204.5057 (2012) - 2011
- [i2]Tomás Brázdil, Jan Krcál, Jan Kretínský, Antonín Kucera, Vojtech Rehák:
Measuring Performance of Continuous-Time Stochastic Processes using Timed Automata. CoRR abs/1101.4204 (2011) - [i1]Tomás Brázdil, Jan Krcál, Jan Kretínský, Vojtech Rehák:
Fixed-delay Events in Generalized Semi-Markov Processes Revisited. CoRR abs/1106.1424 (2011)
Coauthor Index
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-23 19:29 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint