Jan Kretínský

Orcid: 0000-0002-8122-2881

Affiliations:
  • Masaryk University, Brno, Czech Republic
  • Technical University of Munich, Department of Informatics, Germany


According to our database1, Jan Kretínský authored at least 116 papers between 2008 and 2024.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Learning Algorithms for Verification of Markov Decision Processes.
CoRR, 2024

Learning Explainable and Better Performing Representations of POMDP Strategies.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2024

2023
Algebraically explainable controllers: decision trees and support vector machines join forces.
Int. J. Softw. Tools Technol. Transf., June, 2023

MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints.
CoRR, 2023

Welcome Remarks from AISoLA 2023/Track C2 Chairs.
Proceedings of the Bridging the Gap Between AI and Reality, 2023

Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives.
LICS, 2023

Learning Attack Trees by Genetic Algorithms.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2023, 2023

Runtime Monitoring for Out-of-Distribution Detection in Object Detection Neural Networks.
Proceedings of the Formal Methods - 25th International Symposium, 2023

Guessing Winning Policies in LTL Synthesis by Semantic Learning.
Proceedings of the Computer Aided Verification - 35th International Conference, 2023

Syntactic vs Semantic Linear Abstraction and Refinement of Neural Networks.
Proceedings of the Automated Technology for Verification and Analysis, 2023

2022
From linear temporal logic and limit-deterministic Büchi automata to deterministic parity automata.
Int. J. Softw. Tools Technol. Transf., 2022

Value iteration for simple stochastic games: Stopping criterion and learning algorithm.
Inf. Comput., 2022

PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP.
CoRR, 2022

Index appearance record with preorders.
Acta Informatica, 2022

Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2022

Planning via model checking with decision-tree controllers.
Proceedings of the 2022 International Conference on Robotics and Automation, 2022

Anytime Guarantees for Reachability in Uncountable Markov Decision Processes.
Proceedings of the 33rd International Conference on Concurrency Theory, 2022

Abstraction-Based Segmental Simulation of Chemical Reaction Networks.
Proceedings of the Computational Methods in Systems Biology, 2022

PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP.
Proceedings of the Computer Aided Verification - 34th International Conference, 2022

Satisfiability of Quantitative Probabilistic CTL: Rise to the Challenge.
Proceedings of the Principles of Systems Design, 2022

Optimistic and Topological Value Iteration for Simple Stochastic Games.
Proceedings of the Automated Technology for Verification and Analysis, 2022

2021
Formalizing and guaranteeing human-robot interaction.
Commun. ACM, 2021

dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2021

Gaussian-Based Runtime Detection of Out-of-distribution Inputs for Neural Networks.
Proceedings of the Runtime Verification - 21st International Conference, 2021

Semantic Abstraction-Guided Motion Planning for scLTL Missions in Unknown Environments.
Proceedings of the Robotics: Science and Systems XVII, Virtual Event, July 12-16, 2021., 2021

LTL-Constrained Steady-State Policy Synthesis.
Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, 2021

Assessing Security of Cryptocurrencies with Attack-Defense Trees: Proof of Concept and Future Directions.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2021, 2021

Enforcing ω-Regular Properties in Markov Chains by Restarting.
Proceedings of the 32nd International Conference on Concurrency Theory, 2021

Guaranteed Trade-Offs in Dynamic Information Flow Tracking Games.
Proceedings of the 2021 60th IEEE Conference on Decision and Control (CDC), 2021

2020
Of Cores: A Partial-Exploration Framework for Markov Decision Processes.
Log. Methods Comput. Sci., 2020

A Unified Translation of Linear Temporal Logic to ω-Automata.
J. ACM, 2020

Logical vs. behavioural specifications.
Inf. Comput., 2020

Online Monitoring ω-Regular Properties in Unknown Markov Chains.
CoRR, 2020

Comparison of Algorithms for Simple Stochastic Games.
Proceedings of the Proceedings 11th International Symposium on Games, 2020

Comparison of Algorithms for Simple Stochastic Games (Full Version).
CoRR, 2020

An Anytime Algorithm for Reachability on Uncountable MDP.
CoRR, 2020

Finite-Memory Near-Optimal Learning for Markov Decision Processes with Long-Run Average Reward.
Proceedings of the Thirty-Sixth Conference on Uncertainty in Artificial Intelligence, 2020

Approximating Values of Generalized-Reachability Stochastic Games.
Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends, 2020

Statistical Model Checking: Black or White?
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles, 2020

dtControl: decision tree learning algorithms for controller representation.
Proceedings of the HSCC '20: 23rd ACM International Conference on Hybrid Systems: Computation and Control, 2020

Automata Tutor v3.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks.
Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

DeepAbstract: Neural Network Abstraction for Accelerating Verification.
Proceedings of the Automated Technology for Verification and Analysis, 2020

2019
Stopping Criteria for Value and Strategy Iteration on Concurrent Stochastic Reachability Games.
CoRR, 2019

Approximating Values of Generalized-Reachability Stochastic Games.
CoRR, 2019

The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report).
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2019

Expected Cost Analysis of Attack-Defense Trees.
Proceedings of the Quantitative Evaluation of Systems, 16th International Conference, 2019

SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processes.
Proceedings of the Quantitative Evaluation of Systems, 16th International Conference, 2019

Strategy Representation by Decision Trees with Linear Classifiers.
Proceedings of the Quantitative Evaluation of Systems, 16th International Conference, 2019

Semi-quantitative Abstraction and Analysis of Chemical Reaction Networks (Extended Abstract).
Proceedings of the Computational Methods in Systems Biology, 2019

Satisfiability Bounds for ω-Regular Properties in Bounded-Parameter Markov Decision Processes.
Proceedings of the 58th IEEE Conference on Decision and Control, 2019

Semi-quantitative Abstraction and Analysis of Chemical Reaction Networks.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games.
Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis.
Proceedings of the Automated Technology for Verification and Analysis, 2019

2018
Compositionality for quantitative specifications.
Soft Comput., 2018

Machine Learning and Model Checking Join Forces (Dagstuhl Seminar 18121).
Dagstuhl Reports, 2018

LTL Store: Repository of LTL formulae from literature and case studies.
CoRR, 2018

Strategy Representation by Decision Trees in Reactive Synthesis.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification, 2018

The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL.
Proceedings of the 29th International Conference on Concurrency Theory, 2018

Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints.
Proceedings of the 29th International Conference on Concurrency Theory, 2018

Rabinizer 4: From LTL to Your Favourite Deterministic Automaton.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm.
Proceedings of the Computer Aided Verification - 30th International Conference, 2018

Owl: A Library for ω-Words, Automata, and LTL.
Proceedings of the Automated Technology for Verification and Analysis, 2018

Continuous-Time Markov Decisions Based on Partial Exploration.
Proceedings of the Automated Technology for Verification and Analysis, 2018

2017
Faster Statistical Model Checking for Unbounded Temporal Properties.
ACM Trans. Comput. Log., 2017

Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.
Log. Methods Comput. Sci., 2017

Index Appearance Record for Transforming Rabin Automata into Parity Automata.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Value Iteration for Long-Run Average Reward in Markov Decision Processes.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

30 Years of Modal Transition Systems: Survey of Extensions and Analysis.
Proceedings of the Models, Algorithms, Logics and Tools, 2017

Efficient Strategy Iteration for Mean Payoff in Markov Decision Processes.
Proceedings of the Automated Technology for Verification and Analysis, 2017

2016
From LTL to deterministic automata - A safraless compositional approach.
Formal Methods Syst. Des., 2016

Survey of Statistical Verification of Linear Unbounded Properties: Model Checking and Distances.
Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, 2016

Linear Distances between Markov Chains.
Proceedings of the 27th International Conference on Concurrency Theory, 2016

Limit-Deterministic Büchi Automata for Linear Temporal Logic.
Proceedings of the Computer Aided Verification - 28th International Conference, 2016

MoChiBA: Probabilistic LTL Model Checking Using Limit-Deterministic Büchi Automata.
Proceedings of the Automated Technology for Verification and Analysis, 2016

2015
Verification of Discrete- and Continuous-Time Non-Deterministic Markovian Systems (Verifikation von non-deterministischen Markovischen Systemen mit diskreter oder kontinuierlicher Zeit)
PhD thesis, 2015

Controller synthesis for MDPs and Frequency LTL$\setminus$GU.
CoRR, 2015

Refinement checking on parametric modal transition systems.
Acta Informatica, 2015

Controller Synthesis for MDPs and Frequency LTL<sub>\GU</sub>.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games.
Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, 2015

Polynomial Time Decidability of Weighted Synchronization under Partial Observability.
Proceedings of the 26th International Conference on Concurrency Theory, 2015

Complete Composition Operators for IOCO-Testing Theory.
Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering, 2015

Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

The Hanoi Omega-Automata Format.
Proceedings of the Computer Aided Verification - 27th International Conference, 2015

2014
Probabilistic Bisimulation: Naturally on Distributions.
Proceedings of the CONCUR 2014 - Concurrency Theory - 25th International Conference, 2014

From LTL to Deterministic Automata: A Safraless Compositional Approach.
Proceedings of the Computer Aided Verification - 26th International Conference, 2014

Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata.
Proceedings of the Automated Technology for Verification and Analysis, 2014

Verification of Markov Decision Processes Using Learning Algorithms.
Proceedings of the Automated Technology for Verification and Analysis, 2014

2013
Continuous-time stochastic games with time-bounded reachability.
Inf. Comput., 2013

On time-average limits in deterministic and stochastic petri nets.
Proceedings of the ACM/SPEC International Conference on Performance Engineering, 2013

On Refinements of Boolean and Parametric Modal Transition Systems.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2013, 2013

Compositional Verification and Optimization of Interactive Markov Chains.
Proceedings of the CONCUR 2013 - Concurrency Theory - 24th International Conference, 2013

Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory.
Proceedings of the CONCUR 2013 - Concurrency Theory - 24th International Conference, 2013

Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

MoTraS: A Tool for Modal Transition Systems and Their Extensions.
Proceedings of the Automated Technology for Verification and Analysis, 2013

Rabinizer 2: Small Deterministic Automata for LTL ∖ GU.
Proceedings of the Automated Technology for Verification and Analysis, 2013

2012
EXPTIME-completeness of thorough refinement on modal transition systems.
Inf. Comput., 2012

Dual-Priced Modal Transition Systems with Time Durations.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2012

Modal Process Rewrite Systems.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2012, 2012

Verification of Open Interactive Markov Chains.
Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2012

Deterministic Automata for the (F, G)-Fragment of LTL.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

Rabinizer: Small Deterministic Automata for LTL(F, G).
Proceedings of the Automated Technology for Verification and Analysis, 2012

2011
Measuring performance of continuous-time stochastic processes using timed automata.
Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, 2011

Fixed-Delay Events in Generalized Semi-Markov Processes Revisited.
Proceedings of the CONCUR 2011 - Concurrency Theory - 22nd International Conference, 2011

Parametric Modal Transition Systems.
Proceedings of the Automated Technology for Verification and Analysis, 2011

Modal Transition Systems: Composition and LTL Model Checking.
Proceedings of the Automated Technology for Verification and Analysis, 2011

2010
Process Algebra for Modal Transition Systemses.
Proceedings of the Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, 2010

Stochastic Real-Time Games with Qualitative Timed Automata Objectives.
Proceedings of the CONCUR 2010 - Concurrency Theory, 21th International Conference, 2010

2009
On determinism in modal transition systems.
Theor. Comput. Sci., 2009

Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete.
Proceedings of the Theoretical Aspects of Computing, 2009

2008
The Satisfiability Problem for Probabilistic CTL.
Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, 2008


  Loading...