# Jan Kretínský

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

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

Book
In proceedings
Article
PhD thesis
Other

## Bibliography

2018
Compositionality for quantitative specifications.
Soft Comput., 2018

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

Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes.
CoRR, 2018

Continuous-Time Markov Decisions based on Partial Exploration.
CoRR, 2018

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

The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL.
CoRR, 2018

Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes.
CoRR, 2018

One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata.
CoRR, 2018

Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints.
CoRR, 2018

Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm.
CoRR, 2018

Strategy Representation by Decision Trees in Reactive Synthesis.
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 \omega -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.
Logical Methods in Computer Science, 2017

Index appearance record for transforming Rabin automata into parity automata.
CoRR, 2017

Efficient Strategy Iteration for Mean Payoff in Markov Decision Processes.
CoRR, 2017

From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata.
CoRR, 2017

Value Iteration for Long-run Average Reward in Markov Decision Processes.
CoRR, 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 in System Design, 2016

Linear Distances between Markov Chains.
CoRR, 2016

Faster Statistical Model Checking for Unbounded Temporal Properties.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 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
Controller synthesis for MDPs and Frequency LTL$\setminus$GU.
CoRR, 2015

Faster Statistical Model Checking for Unbounded Temporal Properties.
CoRR, 2015

Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.
CoRR, 2015

Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.
CoRR, 2015

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

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

Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes.
Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 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
Temporal Logic Control for Stochastic Linear Systems using Abstraction Refinement of Probabilistic Games.
CoRR, 2014

Probabilistic Bisimulation: Naturally on Distributions.
CoRR, 2014

Compositionality for Quantitative Specifications.
CoRR, 2014

From LTL to Deterministic Automata: A Safraless Compositional Approach.
CoRR, 2014

Verification of Markov Decision Processes using Learning Algorithms.
CoRR, 2014

Compositionality for Quantitative Specifications.
Proceedings of the Formal Aspects of Component Software - 11th International Symposium, 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

Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis
CoRR, 2013

On Refinements of Boolean and Parametric Modal Transition Systems
CoRR, 2013

Compositional Verification and Optimization of Interactive Markov Chains.
CoRR, 2013

Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory.
CoRR, 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

Deterministic Automata for the (F,G)-fragment of LTL
CoRR, 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
Fixed-delay Events in Generalized Semi-Markov Processes Revisited
CoRR, 2011

Measuring Performance of Continuous-Time Stochastic Processes using Timed Automata
CoRR, 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

Continuous-Time Stochastic Games with Time-Bounded Reachability.
Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2009

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