Jan Kretinsky

Henzinger_Thomas Group
Chatterjee Group

30 Publications

Mark all

[30]
2025 | Published | Conference Paper | IST-REx-ID: 19375 | OA
Azeem, Muqsit, et al. “1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization.” 26th International Conference on Verification, Model Checking, and Abstract Interpretation, vol. 15530, Springer Nature, 2025, pp. 97–120, doi:10.1007/978-3-031-82703-7_5.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[29]
2024 | Published | Conference Paper | IST-REx-ID: 18600 | OA
Andriushchenko, Roman, Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. TOOLympics Challenge 2023 14550. 2024
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[28]
2023 | Published | Conference Paper | IST-REx-ID: 14259 | OA
Kretinsky, Jan, et al. “Guessing Winning Policies in LTL Synthesis by Semantic Learning.” 35th International Conference on Computer Aided Verification , vol. 13964, Springer Nature, 2023, pp. 390–414, doi:10.1007/978-3-031-37706-8_20.
[Published Version] View | Files available | DOI
 
[27]
2023 | Published | Conference Paper | IST-REx-ID: 13967 | OA
Kretinsky, Jan, Stopping criteria for value iteration on stochastic games with quantitative objectives. 38th Annual ACM/IEEE Symposium on Logic in Computer Science 2023. 2023
[Preprint] View | DOI | Download Preprint (ext.) | WoS | arXiv
 
[26]
2022 | Published | Conference Paper | IST-REx-ID: 12775 | OA
Grover, Kush, et al. “Anytime Guarantees for Reachability in Uncountable Markov Decision Processes.” 33rd International Conference on Concurrency Theory , vol. 243, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, doi:10.4230/LIPIcs.CONCUR.2022.11.
[Published Version] View | Files available | DOI | arXiv
 
[25]
2022 | Published | Journal Article | IST-REx-ID: 10602 | OA
Kretinsky, Jan, et al. “Index Appearance Record with Preorders.” Acta Informatica, vol. 59, Springer Nature, 2022, pp. 585–618, doi:10.1007/s00236-021-00412-y.
[Published Version] View | Files available | DOI | WoS
 
[24]
2018 | Published | Conference Paper | IST-REx-ID: 297 | OA
Brázdil, Tomáš, et al. Strategy Representation by Decision Trees in Reactive Synthesis. Vol. 10805, Springer, 2018, pp. 385–407, doi:10.1007/978-3-319-89960-2_21.
[Published Version] View | Files available | DOI | WoS
 
[23]
2017 | Published | Conference Paper | IST-REx-ID: 13160 | OA
Kretinsky, Jan, et al. “Index Appearance Record for Transforming Rabin Automata into Parity Automata.” Tools and Algorithms for the Construction and Analysis of Systems, vol. 10205, Springer, 2017, pp. 443–60, doi:10.1007/978-3-662-54577-5_26.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[22]
2017 | Published | Journal Article | IST-REx-ID: 1407 | OA
Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” Nonlinear Analysis: Hybrid Systems, vol. 23, no. 2, Elsevier, 2017, pp. 230–53, doi:10.1016/j.nahs.2016.04.006.
[Preprint] View | Files available | DOI | Download Preprint (ext.) | WoS | arXiv
 
[21]
2017 | Published | Conference Paper | IST-REx-ID: 645 | OA
Ashok, Pranav, et al. Value Iteration for Long Run Average Reward in Markov Decision Processes. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10426, Springer, 2017, pp. 201–21, doi:10.1007/978-3-319-63387-9_10.
[Submitted Version] View | DOI | Download Submitted Version (ext.) | arXiv
 
[20]
2017 | Published | Journal Article | IST-REx-ID: 471 | OA
Daca, Przemyslaw, et al. “Faster Statistical Model Checking for Unbounded Temporal Properties.” ACM Transactions on Computational Logic, vol. 18, no. 2, 12, ACM, 2017, doi:10.1145/3060139.
[Submitted Version] View | Files available | DOI | Download Submitted Version (ext.) | arXiv
 
[19]
2017 | Published | Journal Article | IST-REx-ID: 466 | OA
Chatterjee, Krishnendu, Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science 13 (2). 2017
[Published Version] View | Files available | DOI
 
[18]
2016 | Published | Conference Paper | IST-REx-ID: 1093 | OA
Daca, Przemyslaw, et al. Linear Distances between Markov Chains. Vol. 59, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.CONCUR.2016.20.
[Published Version] View | Files available | DOI
 
[17]
2016 | Published | Conference Paper | IST-REx-ID: 1234 | OA
Daca, Przemyslaw, et al. Faster Statistical Model Checking for Unbounded Temporal Properties. Vol. 9636, Springer, 2016, pp. 112–29, doi:10.1007/978-3-662-49674-9_7.
[Preprint] View | Files available | DOI | Download Preprint (ext.) | arXiv
 
[16]
2015 | Published | Journal Article | IST-REx-ID: 1846 | OA
Beneš, Nikola, et al. “Refinement Checking on Parametric Modal Transition Systems.” Acta Informatica, vol. 52, no. 2–3, Springer, 2015, pp. 269–97, doi:10.1007/s00236-015-0215-4.
[Submitted Version] View | Files available | DOI
 
[15]
2015 | Published | Conference Paper | IST-REx-ID: 1601 | OA
Babiak, Tomáš, et al. The Hanoi Omega-Automata Format. Vol. 9206, Springer, 2015, pp. 479–86, doi:10.1007/978-3-319-21690-4_31.
[Submitted Version] View | Files available | DOI
 
[14]
2015 | Published | Conference Paper | IST-REx-ID: 1499 | OA
Kretinsky, Jan, et al. Polynomial Time Decidability of Weighted Synchronization under Partial Observability. Vol. 42, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–54, doi:10.4230/LIPIcs.CONCUR.2015.142.
[Published Version] View | Files available | DOI
 
[13]
2015 | Published | Conference Paper | IST-REx-ID: 1502 | OA
Beneš, Nikola, et al. Complete Composition Operators for IOCO-Testing Theory. ACM, 2015, pp. 101–10, doi:10.1145/2737166.2737175.
[Submitted Version] View | Files available | DOI
 
[12]
2015 | Published | Conference Paper | IST-REx-ID: 1594
Forejt, Vojtěch, et al. Controller Synthesis for MDPs and Frequency LTL\GU. Vol. 9450, Springer, 2015, pp. 162–77, doi:10.1007/978-3-662-48899-7_12.
View | DOI
 
[11]
2015 | Published | Conference Paper | IST-REx-ID: 1689 | OA
Svoreňová, Mária, et al. “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, ACM, 2015, pp. 259–68, doi:10.1145/2728606.2728608.
[Preprint] View | Files available | DOI | Download Preprint (ext.) | arXiv
 
[10]
2015 | Published | Conference Paper | IST-REx-ID: 1603 | OA
Brázdil, Tomáš, et al. Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. Vol. 9206, Springer, 2015, pp. 158–77, doi:10.1007/978-3-319-21690-4_10.
[Preprint] View | Files available | DOI | Download Preprint (ext.) | arXiv
 
[9]
2015 | Published | Conference Paper | IST-REx-ID: 1882 | OA
Fahrenberg, Uli, et al. Compositionality for Quantitative Specifications. Vol. 8997, Springer, 2015, pp. 306–24, doi:10.1007/978-3-319-15317-9_19.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[8]
2015 | Published | Conference Paper | IST-REx-ID: 1657 | OA
Chatterjee, Krishnendu, et al. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IEEE, 2015, pp. 244–56, doi:10.1109/LICS.2015.32.
[Preprint] View | Files available | DOI | Download Preprint (ext.)
 
[7]
2015 | Published | Technical Report | IST-REx-ID: 5429 | OA
Chatterjee, Krishnendu, et al. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IST Austria, 2015, doi:10.15479/AT:IST-2015-318-v1-1.
[Published Version] View | Files available | DOI
 
[6]
2015 | Published | Technical Report | IST-REx-ID: 5435 | OA
Chatterjee, Krishnendu, et al. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IST Austria, 2015, doi:10.15479/AT:IST-2015-318-v2-1.
[Published Version] View | Files available | DOI
 
[5]
2014 | Published | Conference Paper | IST-REx-ID: 2026
Komárková, Zuzana, and Jan Kretinsky. “Rabinizer 3: Safraless Translation of Ltl to Small Deterministic Automata.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, vol. 8837, Springer, 2014, pp. 235–41, doi:10.1007/978-3-319-11936-6_17.
View | DOI
 
[4]
2014 | Published | Conference Paper | IST-REx-ID: 2053 | OA
Hermanns, Holger, et al. “Probabilistic Bisimulation: Naturally on Distributions.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan and Daniele Gorla, vol. 8704, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 249–65, doi:10.1007/978-3-662-44584-6_18.
[Submitted Version] View | DOI | Download Submitted Version (ext.) | arXiv
 
[3]
2014 | Published | Conference Paper | IST-REx-ID: 2027 | OA
Brázdil, Tomáš, et al. “Verification of Markov Decision Processes Using Learning Algorithms.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, vol. 8837, Springer, 2014, pp. 98–114, doi:10.1007/978-3-319-11936-6_8.
[Submitted Version] View | DOI | Download Submitted Version (ext.) | arXiv
 
[2]
2014 | Published | Conference Paper | IST-REx-ID: 2190 | OA
Esparza, Javier, and Jan Kretinsky. From LTL to Deterministic Automata: A Safraless Compositional Approach. Vol. 8559, Springer, 2014, pp. 192–208, doi:10.1007/978-3-319-08867-9_13.
[Submitted Version] View | DOI | Download Submitted Version (ext.) | arXiv
 
[1]
2013 | Published | Conference Paper | IST-REx-ID: 2446 | OA
Chatterjee, Krishnendu, et al. Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. Vol. 8044, Springer, 2013, pp. 559–75, doi:10.1007/978-3-642-39799-8_37.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
Marked Publication(s)

Search

Filter Publications

Display / Sort

Citation Style: MLA

Export / Embed

Grants


30 Publications

Mark all

[30]
2025 | Published | Conference Paper | IST-REx-ID: 19375 | OA
Azeem, Muqsit, et al. “1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization.” 26th International Conference on Verification, Model Checking, and Abstract Interpretation, vol. 15530, Springer Nature, 2025, pp. 97–120, doi:10.1007/978-3-031-82703-7_5.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[29]
2024 | Published | Conference Paper | IST-REx-ID: 18600 | OA
Andriushchenko, Roman, Tools at the Frontiers of Quantitative Verification: QComp 2023 Competition Report. TOOLympics Challenge 2023 14550. 2024
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[28]
2023 | Published | Conference Paper | IST-REx-ID: 14259 | OA
Kretinsky, Jan, et al. “Guessing Winning Policies in LTL Synthesis by Semantic Learning.” 35th International Conference on Computer Aided Verification , vol. 13964, Springer Nature, 2023, pp. 390–414, doi:10.1007/978-3-031-37706-8_20.
[Published Version] View | Files available | DOI
 
[27]
2023 | Published | Conference Paper | IST-REx-ID: 13967 | OA
Kretinsky, Jan, Stopping criteria for value iteration on stochastic games with quantitative objectives. 38th Annual ACM/IEEE Symposium on Logic in Computer Science 2023. 2023
[Preprint] View | DOI | Download Preprint (ext.) | WoS | arXiv
 
[26]
2022 | Published | Conference Paper | IST-REx-ID: 12775 | OA
Grover, Kush, et al. “Anytime Guarantees for Reachability in Uncountable Markov Decision Processes.” 33rd International Conference on Concurrency Theory , vol. 243, 11, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, doi:10.4230/LIPIcs.CONCUR.2022.11.
[Published Version] View | Files available | DOI | arXiv
 
[25]
2022 | Published | Journal Article | IST-REx-ID: 10602 | OA
Kretinsky, Jan, et al. “Index Appearance Record with Preorders.” Acta Informatica, vol. 59, Springer Nature, 2022, pp. 585–618, doi:10.1007/s00236-021-00412-y.
[Published Version] View | Files available | DOI | WoS
 
[24]
2018 | Published | Conference Paper | IST-REx-ID: 297 | OA
Brázdil, Tomáš, et al. Strategy Representation by Decision Trees in Reactive Synthesis. Vol. 10805, Springer, 2018, pp. 385–407, doi:10.1007/978-3-319-89960-2_21.
[Published Version] View | Files available | DOI | WoS
 
[23]
2017 | Published | Conference Paper | IST-REx-ID: 13160 | OA
Kretinsky, Jan, et al. “Index Appearance Record for Transforming Rabin Automata into Parity Automata.” Tools and Algorithms for the Construction and Analysis of Systems, vol. 10205, Springer, 2017, pp. 443–60, doi:10.1007/978-3-662-54577-5_26.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[22]
2017 | Published | Journal Article | IST-REx-ID: 1407 | OA
Svoreňová, Mária, et al. “Temporal Logic Control for Stochastic Linear Systems Using Abstraction Refinement of Probabilistic Games.” Nonlinear Analysis: Hybrid Systems, vol. 23, no. 2, Elsevier, 2017, pp. 230–53, doi:10.1016/j.nahs.2016.04.006.
[Preprint] View | Files available | DOI | Download Preprint (ext.) | WoS | arXiv
 
[21]
2017 | Published | Conference Paper | IST-REx-ID: 645 | OA
Ashok, Pranav, et al. Value Iteration for Long Run Average Reward in Markov Decision Processes. Edited by Rupak Majumdar and Viktor Kunčak, vol. 10426, Springer, 2017, pp. 201–21, doi:10.1007/978-3-319-63387-9_10.
[Submitted Version] View | DOI | Download Submitted Version (ext.) | arXiv
 
[20]
2017 | Published | Journal Article | IST-REx-ID: 471 | OA
Daca, Przemyslaw, et al. “Faster Statistical Model Checking for Unbounded Temporal Properties.” ACM Transactions on Computational Logic, vol. 18, no. 2, 12, ACM, 2017, doi:10.1145/3060139.
[Submitted Version] View | Files available | DOI | Download Submitted Version (ext.) | arXiv
 
[19]
2017 | Published | Journal Article | IST-REx-ID: 466 | OA
Chatterjee, Krishnendu, Unifying two views on multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science 13 (2). 2017
[Published Version] View | Files available | DOI
 
[18]
2016 | Published | Conference Paper | IST-REx-ID: 1093 | OA
Daca, Przemyslaw, et al. Linear Distances between Markov Chains. Vol. 59, 20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.CONCUR.2016.20.
[Published Version] View | Files available | DOI
 
[17]
2016 | Published | Conference Paper | IST-REx-ID: 1234 | OA
Daca, Przemyslaw, et al. Faster Statistical Model Checking for Unbounded Temporal Properties. Vol. 9636, Springer, 2016, pp. 112–29, doi:10.1007/978-3-662-49674-9_7.
[Preprint] View | Files available | DOI | Download Preprint (ext.) | arXiv
 
[16]
2015 | Published | Journal Article | IST-REx-ID: 1846 | OA
Beneš, Nikola, et al. “Refinement Checking on Parametric Modal Transition Systems.” Acta Informatica, vol. 52, no. 2–3, Springer, 2015, pp. 269–97, doi:10.1007/s00236-015-0215-4.
[Submitted Version] View | Files available | DOI
 
[15]
2015 | Published | Conference Paper | IST-REx-ID: 1601 | OA
Babiak, Tomáš, et al. The Hanoi Omega-Automata Format. Vol. 9206, Springer, 2015, pp. 479–86, doi:10.1007/978-3-319-21690-4_31.
[Submitted Version] View | Files available | DOI
 
[14]
2015 | Published | Conference Paper | IST-REx-ID: 1499 | OA
Kretinsky, Jan, et al. Polynomial Time Decidability of Weighted Synchronization under Partial Observability. Vol. 42, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pp. 142–54, doi:10.4230/LIPIcs.CONCUR.2015.142.
[Published Version] View | Files available | DOI
 
[13]
2015 | Published | Conference Paper | IST-REx-ID: 1502 | OA
Beneš, Nikola, et al. Complete Composition Operators for IOCO-Testing Theory. ACM, 2015, pp. 101–10, doi:10.1145/2737166.2737175.
[Submitted Version] View | Files available | DOI
 
[12]
2015 | Published | Conference Paper | IST-REx-ID: 1594
Forejt, Vojtěch, et al. Controller Synthesis for MDPs and Frequency LTL\GU. Vol. 9450, Springer, 2015, pp. 162–77, doi:10.1007/978-3-662-48899-7_12.
View | DOI
 
[11]
2015 | Published | Conference Paper | IST-REx-ID: 1689 | OA
Svoreňová, Mária, et al. “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, ACM, 2015, pp. 259–68, doi:10.1145/2728606.2728608.
[Preprint] View | Files available | DOI | Download Preprint (ext.) | arXiv
 
[10]
2015 | Published | Conference Paper | IST-REx-ID: 1603 | OA
Brázdil, Tomáš, et al. Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. Vol. 9206, Springer, 2015, pp. 158–77, doi:10.1007/978-3-319-21690-4_10.
[Preprint] View | Files available | DOI | Download Preprint (ext.) | arXiv
 
[9]
2015 | Published | Conference Paper | IST-REx-ID: 1882 | OA
Fahrenberg, Uli, et al. Compositionality for Quantitative Specifications. Vol. 8997, Springer, 2015, pp. 306–24, doi:10.1007/978-3-319-15317-9_19.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
[8]
2015 | Published | Conference Paper | IST-REx-ID: 1657 | OA
Chatterjee, Krishnendu, et al. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IEEE, 2015, pp. 244–56, doi:10.1109/LICS.2015.32.
[Preprint] View | Files available | DOI | Download Preprint (ext.)
 
[7]
2015 | Published | Technical Report | IST-REx-ID: 5429 | OA
Chatterjee, Krishnendu, et al. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IST Austria, 2015, doi:10.15479/AT:IST-2015-318-v1-1.
[Published Version] View | Files available | DOI
 
[6]
2015 | Published | Technical Report | IST-REx-ID: 5435 | OA
Chatterjee, Krishnendu, et al. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. IST Austria, 2015, doi:10.15479/AT:IST-2015-318-v2-1.
[Published Version] View | Files available | DOI
 
[5]
2014 | Published | Conference Paper | IST-REx-ID: 2026
Komárková, Zuzana, and Jan Kretinsky. “Rabinizer 3: Safraless Translation of Ltl to Small Deterministic Automata.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, vol. 8837, Springer, 2014, pp. 235–41, doi:10.1007/978-3-319-11936-6_17.
View | DOI
 
[4]
2014 | Published | Conference Paper | IST-REx-ID: 2053 | OA
Hermanns, Holger, et al. “Probabilistic Bisimulation: Naturally on Distributions.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Paolo Baldan and Daniele Gorla, vol. 8704, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pp. 249–65, doi:10.1007/978-3-662-44584-6_18.
[Submitted Version] View | DOI | Download Submitted Version (ext.) | arXiv
 
[3]
2014 | Published | Conference Paper | IST-REx-ID: 2027 | OA
Brázdil, Tomáš, et al. “Verification of Markov Decision Processes Using Learning Algorithms.” Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), edited by Franck Cassez and Jean-François Raskin, vol. 8837, Springer, 2014, pp. 98–114, doi:10.1007/978-3-319-11936-6_8.
[Submitted Version] View | DOI | Download Submitted Version (ext.) | arXiv
 
[2]
2014 | Published | Conference Paper | IST-REx-ID: 2190 | OA
Esparza, Javier, and Jan Kretinsky. From LTL to Deterministic Automata: A Safraless Compositional Approach. Vol. 8559, Springer, 2014, pp. 192–208, doi:10.1007/978-3-319-08867-9_13.
[Submitted Version] View | DOI | Download Submitted Version (ext.) | arXiv
 
[1]
2013 | Published | Conference Paper | IST-REx-ID: 2446 | OA
Chatterjee, Krishnendu, et al. Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. Vol. 8044, Springer, 2013, pp. 559–75, doi:10.1007/978-3-642-39799-8_37.
[Preprint] View | DOI | Download Preprint (ext.) | arXiv
 
Marked Publication(s)

Search

Filter Publications

Display / Sort

Citation Style: MLA

Export / Embed