Výpis publikací

KŘETÍNSKÝ, Jan; Sabine RIEDER; Gesina SCHWALBE a Youssef SHOEB. Hidden-Layer Monitoring for Out-of-Distribution Localization in Image Segmentation. Online. In International Conference on Runtime Verification. Cham: Springer, 2026, s. 274-295. ISBN 978-3-032-05434-0.

DORFHUBER, Florian Sebastian; Marisol BARRIENTOS; Julia EISENTRAUT; Jan KŘETÍNSKÝ a Jana HALÁMKOVÁ. Keep it simple, or teach them logics: Attack-Defense Tree Perception by Laypeople. In The 11th International Symposium on Dependable Software Engineering Theories, Tools and Applications. Oxford: Springer, 2026, 21 s. ISSN 0302-9743.

KANAV, Sudeep; Jan KŘETÍNSKÝ a Sabine RIEDER. A Literature Review on Verification and Abstraction of Neural Networks Within the Formal Methods Community. In Principles of Verification: Cycling the Probabilistic Landscape : Essays Dedicated to Joost-Pieter Katoen on the Occasion of His 60th Birthday. Cham, Switzerland: Springer, 2025, s. 39-65. Lecture Notes in Computer Science, 15262. ISBN 978-3-031-75777-8. Dostupné z: https://doi.org/10.1007/978-3-031-75778-5_3.

RIEDER, Sabine; Stefan PRANGER; Debraj CHAKRABORTY; Jan KŘETÍNSKÝ a Bettina KÖNIGHOFER. Explainably Safe Reinforcement Learning. Online. In The Thirty-ninth Annual Conference on Neural Information Processing Systems. United States of America: Neural Information Processing Systems Foundation, Inc., 2025, s. 1-30. ISSN 1049-5258.

CHAKRABORTY, Debraj; Clemens DUBSLAFF; Sudeep KANAV; Jan KŘETÍNSKÝ a Christoph WEINHUBER. Explaining Control Policies through Predicate Decision Diagrams. In HSCC '25: Proceedings of the 28th ACM International Conference on Hybrid Systems: Computation and Control. Irvine, USA: Association for Computing Machinery, 2025, s. 1-12. ISBN 979-8-4007-1504-4. Dostupné z: https://doi.org/10.1145/3716863.3718049.

HASHEMI, Vahid; Jan KŘETÍNSKÝ; Sabine RIEDER; Torsten SCHÖN a Jan VORHOFF. Gaussian-Based and Outside-the-Box Runtime Monitoring Join Forces. Online. In RV 2024, 24th International Conference on Runtime Verification. Cham: Springer, 2025, s. 218-228. ISBN 978-3-031-74233-0. Dostupné z: https://doi.org/10.1007/978-3-031-74234-7_14.

BRÁZDIL, Tomáš; Krishnendu CHATTERJEE; Martin CHMELÍK; Vojtěch FOREJT; Jan KŘETÍNSKÝ; Marta KWIATKOWSKA; Tobias MEGGENDORFER; David PARKER a Mateusz UJMA. Learning Algorithms for Verification of Markov Decision Processes. TheoretiCS. 2025, roč. 4, č. 13268, s. 1-82. ISSN 2751-4838. Dostupné z: https://doi.org/10.46298/theoretics.25.10.

KŘETÍNSKÝ, Jan; Chaitanya AGARWAL; Shibashis GUHA a M. PAZHAMALAI. PAC statistical model checking of mean payoff in discrete- and continuous-time MDP. Springer. 2025, roč. 66, č. 2, s. 195-237. ISSN 0925-9856. Dostupné z: https://doi.org/10.1007/s10703-024-00463-0.

KŘETÍNSKÝ, Jan; Tobias MEGGENDORFER; Maximilian PROKOP a Ashkan ZARKAH. SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning. In Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2025. Cham: Springer, 2025, s. 233-253. ISBN 978-3-031-90642-8.

AZEEM, Muqsit; Jan KŘETÍNSKÝ a Maximilian WEININGER. Sound Value Iteration for Simple Stochastic Games. Online. In ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE. SYDNEY: OPEN PUBL ASSOC, 2025, s. 29-44. ISSN 2075-2180. Dostupné z: https://doi.org/10.4204/EPTCS.428.4.

KANAV, Sudeep; Jan KŘETÍNSKÝ a Kim G. LARSEN. Statistical Model Checking the 2024 Edition! In Bridging the Gap Between AI and Reality - Second International Conference, AISoLA 2024. Crete, Greece: Springer, 2025, s. 303-311. ISBN 978-3-031-75433-3. Dostupné z: https://doi.org/10.1007/978-3-031-75434-0_21.

GROBELNA, Marta; Jan KŘETÍNSKÝ a Maximilian WEININGER. Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games. Online. In Stopping Criteria for Value Iteration on Concurrent Stochastic Reachability and Safety Games. Singapore: IEEE, 2025, s. 568-580. ISBN 979-8-3315-7900-5. Dostupné z: https://doi.org/10.1109/LICS65433.2025.00049.

ANDRIUSHCHENKO, Roman; Milan ČEŠKA; Debraj CHAKRABORTY; Sebastian JUNGES; Jan KŘETÍNSKÝ a Filip MACÁK. Symbiotic Local Search for Small Decision Tree Policies in MDPs. In Proceedings of Machine Learning Research, Volume 286: Conference on Uncertainty in Artificial Intelligence (UAI 2025). Rio de Janeiro, Brazil: ML Research Press, 2025, s. 132-148. ISSN 2640-3498.

AZEEM, Muqsit; Debraj CHAKRABORTY; Sudeep KANAV; Jan KŘETÍNSKÝ; Mohammadsadegh MOHAGHEGHI; Stefanie MOHR a Maximilian WEININGER. 1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization. In VMCAI 2025, 26th International Conference on Verification, Model Checking, and Abstract Interpretation. Denver, USA: Springer, 2025, s. 97-120. ISBN 978-3-031-82702-0. Dostupné z: https://doi.org/10.1007/978-3-031-82703-7_5.

HELFRICH, Martin; Roman ANDRIUSHCHENKO; Milan ČEŠKA; Jan KŘETÍNSKÝ; Štefan MARTIČEK a David ŠAFRÁNEK. Abstraction-based segmental simulation of reaction networks using adaptive memoization. BMC Bioinformatics. 2024, roč. 25, č. 350, s. 1-24. ISSN 1471-2105. Dostupné z: https://doi.org/10.1186/s12859-024-05966-5.

BORK, Alexander; Debraj CHAKRABORTY; Kush GROVER; Jan KŘETÍNSKÝ a Stefanie MOHR. Learning Explainable and Better Performing Representations of POMDP Strategies. In TACAS 2024, 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Luxembourg City, Luxembourg: Springer, 2024, s. 299-319. ISBN 978-3-031-57248-7. Dostupné z: https://doi.org/10.1007/978-3-031-57249-4_15.

AZEEM, Muqsit; Marta GROBELNA; Sudeep KANAV; Jan KŘETÍNSKÝ; Stefanie MOHR a Sabine RIEDER. Monitizer: Automating Design and Evaluation of Neural Network Monitors. In CAV 2024, International Conference on Computer Aided Verification. Montreal, Canada: Springer, 2024, s. 265-279. ISBN 978-3-031-65629-3. Dostupné z: https://doi.org/10.1007/978-3-031-65630-9_14.

BALS, Severin; Alexandros EVANGELIDIS; Jan KŘETÍNSKÝ a Jakob WAIBEL. MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints✱. Online. In Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2024. Hong Kong SAR, China: ACM, 2024, s. 1-7. ISBN 979-8-4007-0522-9. Dostupné z: https://doi.org/10.1145/3641513.3650135.

BALS, Severin; Alexandros EVANGELIDIS; Jan KŘETÍNSKÝ a Jakob WAIBEL. Poster Abstract: MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints✱. Online. In Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2024. Hong Kong SAR, China: ACM, 2024, s. 1-2. ISBN 979-8-4007-0522-9. Dostupné z: https://doi.org/10.1145/3641513.3652535.

DORFHUBER, Florian Sebastian; Julia EISENTRAUT; Katharina KLIOBA a Jan KŘETÍNSKÝ. QuADTool: Attack-Defense-Tree Synthesis, Analysis and Bridge to Verification. Online. In International Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems, QEST+FORMATS 2024. Calgary, Canada: Springer, 2024, s. 52-71. ISBN 978-3-031-68415-9. Dostupné z: https://doi.org/10.1007/978-3-031-68416-6_4.

SAVERI, Gaia; Laura NENZI; Luca BORTOLUSSI a Jan KŘETÍNSKÝ. stl2vec: Semantic and Interpretable Vector Representation of Temporal Logic. Online. In ECAI 2024, 27th European Conference on Artificial Intelligence. Santiago de Compostela, Spain: IOS Press, 2024, s. 1381-1388. ISBN 978-1-64368-548-9. Dostupné z: https://doi.org/10.3233/FAIA240638.

KIEFER, Stefan; Jan KŘETÍNSKÝ a Antonín KUČERA. Taming the Infinities of Concurrency : Essays Dedicated to Javier Esparza on the Occasion of His 60th Birthday. Springer, 2024, 309 s. ISBN 978-3-031-56221-1. Dostupné z: https://doi.org/10.1007/978-3-031-56222-8.

JUENGERMANN, Florian; Jan KŘETÍNSKÝ a Maximilian WEININGER. Algebraically explainable controllers: decision trees and support vector machines join forces. International Journal on Software Tools for Technology Transfer. HEIDELBERG: SPRINGER HEIDELBERG, 2023, roč. 25, č. 3, s. 249-266. ISSN 1433-2779. Dostupné z: https://doi.org/10.1007/s10009-023-00716-z.

KŘETÍNSKÝ, Jan; Tobias MEGGENDORFER; Maximilian PROKOP a Sabine RIEDER. Guessing Winning Policies in LTL Synthesis by Semantic Learning. In Constantin Enea and Akash Lal. Computer Aided Verification - 35th International Conference, CAV 2023, Proceedings, Part I. Cham: Springer, 2023, s. 390-414. ISBN 978-3-031-37705-1. Dostupné z: https://doi.org/10.1007/978-3-031-37706-8_20.

DORFHUBER, Florian Sebastian; Julia EISENTRAUT a Jan KŘETÍNSKÝ. Learning Attack Trees by Genetic Algorithms. Online. In Theoretical Aspects of Computing – ICTAC 2023. Lima: Springer, 2023, s. 55-73. ISBN 978-3-031-47962-5. Dostupné z: https://doi.org/10.1007/978-3-031-47963-2_5.

KIESBYE, Jonis; Kush GROVER a Jan KŘETÍNSKÝ. Model Checking for Proving and Improving Fault Tolerance of Satellites. In 978-1-6654-9032-0. 2023 IEEE AEROSPACE CONFERENCE. NEW YORK: IEEE, 2023, 9 s. ISSN 1095-323X. Dostupné z: https://doi.org/10.1109/AERO55745.2023.10115801.

HASHEMI, Vahid; Jan KŘETÍNSKÝ; Sabine RIEDER a Jessica SCHMIDT. Runtime Monitoring for Out-of-Distribution Detection in Object Detection Neural Networks. In 978-3-031-27481-7. FORMAL METHODS, FM 2023. Lübeck: SPRINGER INTERNATIONAL PUBLISHING AG, 2023, s. 622-634. ISBN 978-3-031-27480-0. Dostupné z: https://doi.org/10.1007/978-3-031-27481-7_36.

KŘETÍNSKÝ, Jan; Tobias MEGGENDORFER a Maximilian WEININGER. Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives. In 979-8-3503-3587-3. 2023 38TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, LICS. Boston: IEEE, 2023, s. 1-14. ISBN 979-8-3503-3587-3. Dostupné z: https://doi.org/10.1109/LICS56636.2023.10175771.

CHAU, Calvin; Jan KŘETÍNSKÝ a Stefanie MOHR. Syntactic vs Semantic Linear Abstraction and Refinement of Neural Networks. Online. In Automated Technology for Verification and Analysis. ATVA 2023. Singapore: Springer, 2023, s. 401-421. ISBN 978-3-031-45328-1. Dostupné z: https://doi.org/10.1007/978-3-031-45329-8_19.

HELFRICH, Martin; Milan ČEŠKA; Jan KŘETÍNSKÝ a Stefan MARTICEK. Abstraction-Based Segmental Simulation of Chemical Reaction Networks. In Computational Methods in Systems Biology - 20th International Conference, CMSB 2022, Bucharest, Romania, September 14-16, 2022, Proceedings. Springer, 2022, s. 41-60. ISBN 9783031150333. Dostupné z: https://doi.org/10.1007/978-3-031-15034-0_3.

GROVER, Kush; Jan KŘETÍNSKÝ; Tobias MEGGENDORFER a Maximilian WEININGER. Anytime Guarantees for Reachability in Uncountable Markov Decision Processes. In 33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland. Dagstuhl, 2022, s. 1-20. ISBN 9783959772464. Dostupné z: https://doi.org/10.4230/LIPICS.CONCUR.2022.11.

KŘETÍNSKÝ, Jan; Emanuel RAMNEANTU; Alexander SLIVINSKIY a Maximilian WEININGER. Comparison of algorithms for simple stochastic games. Information and Computation. Amsterdam: Elsevier, 2022, roč. 289, č. 104885, s. 1-23. ISSN 0890-5401. Dostupné z: https://doi.org/10.1016/J.IC.2022.104885.

ESPARZA, Javier; Jan KŘETÍNSKÝ; Jean-François RASKIN a Salomon SICKERT. From linear temporal logic and limit-deterministic Büchi automata to deterministic parity automata. International Journal on Software Tools for Technology Transfer. HEIDELBERG: SPRINGER HEIDELBERG, 2022, roč. 24, č. 4, s. 635-659. ISSN 1433-2779. Dostupné z: https://doi.org/10.1007/S10009-022-00663-1.

KŘETÍNSKÝ, Jan; Tobias MEGGENDORFER; Clara WALDMANN a Maximilian WEININGER. Index appearance record with preorders. Acta informatica. Springer, 2022, roč. 59, č. 5, s. 585-618. ISSN 0001-5903. Dostupné z: https://doi.org/10.1007/S00236-021-00412-Y.

BORTOLUSSI, Luca; Giuseppe Maria GALLO; Jan KŘETÍNSKÝ a Laura NENZI. Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes. In Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I. Springer, 2022, s. 281-300. ISBN 9783030995232. Dostupné z: https://doi.org/10.1007/978-3-030-99524-9_15.

AZEEM, Muqsit; Alexandros EVANGELIDIS; Jan KŘETÍNSKÝ; Alexander SLIVINSKIY a Maximilian WEININGER. Optimistic and Topological Value Iteration for Simple Stochastic Games. In Automated Technology for Verification and Analysis - 20th International Symposium, ATVA 2022, Virtual Event, October 25-28, 2022, Proceedings. Springer, 2022, s. 285-302. ISBN 9783031199912. Dostupné z: https://doi.org/10.1007/978-3-031-19992-9_18.

AGARWAL, Chaitanya; Shibashis GUHA; Jan KŘETÍNSKÝ a Pazhamalai MURUGANANDHAM. PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP. In Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part II. Springer, 2022, s. 3-25. ISBN 9783031131875. Dostupné z: https://doi.org/10.1007/978-3-031-13188-2_1.

KIESBYE, Jonis; Kush GROVER; Pranav ASHOK a Jan KŘETÍNSKÝ. Planning via model checking with decision-tree controllers. In 2022 International Conference on Robotics and Automation, ICRA 2022, Philadelphia, PA, USA, May 23-27, 2022. IEEE, 2022, s. 4347-4354. ISBN 9781728196817. Dostupné z: https://doi.org/10.1109/ICRA46639.2022.9811980.

CHODIL, Miroslav; Antonín KUČERA a Jan KŘETÍNSKÝ. Satisfiability of Quantitative Probabilistic CTL: Rise to the Challenge. In Jean-Francois Raskin, Krishnendu Chatterjee, Laurent Doyen, and Rupak Majumdar. Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday. New York, NY, United States: Springer, 2022, s. 364-387. ISBN 978-3-031-22336-5. Dostupné z: https://doi.org/10.1007/978-3-031-22337-2_18.

EISENTRAUT, Julia; Edon KELMENDI; Jan KŘETÍNSKÝ a Maximilian WEININGER. Value iteration for simple stochastic games: Stopping criterion and learning algorithm. Information and Computation. Amsterdam: Elsevier, 2022, roč. 285, č. 104886, s. 1-32. ISSN 0890-5401. Dostupné z: https://doi.org/10.1016/J.IC.2022.104886.

EISENTRAUT, Julia; Stephan HOLZER; Katharina KLIOBA; Jan KŘETÍNSKÝ; Lukáš PINK a Alexander WAGNER. Assessing Security of Cryptocurrencies with Attack-Defense Trees: Proof of Concept and Future Directions. In Theoretical Aspects of Computing - ICTAC 2021 - 18th International Colloquium, Virtual Event, Nur-Sultan, Kazakhstan, September 8-10, 2021, Proceedings. Springer, 2021, s. 214-234. ISBN 9783030853143. Dostupné z: https://doi.org/10.1007/978-3-030-85315-0_13.

ASHOK, Pranav; Mathias JACKERMEIER; Jan KŘETÍNSKÝ; Christoph WEINHUBER; Maximilian WEININGER a Mayank YADAV. dtControl 2.0: Explainable Strategy Representation via Decision Tree Learning Steered by Experts. In Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II. Springer, 2021, s. 326-345. ISBN 9783030720124. Dostupné z: https://doi.org/10.1007/978-3-030-72013-1_17.

ESPARZA, Javier; Stefan KIEFER; Jan KŘETÍNSKÝ a Maximilian WEININGER. Enforcing ω-Regular Properties in Markov Chains by Restarting. In 32nd International Conference on Concurrency Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference. Dagstuhl, 2021, s. 1-22. ISBN 9783959772037. Dostupné z: https://doi.org/10.4230/LIPICS.CONCUR.2021.5.

KRESS-GAZIT, Hadas; Kerstin EDER; Guy HOFFMAN; Henny ADMONI; Brenna ARGALL; Rüdiger EHLERS; Christoffer HECKMAN; Nils JANSEN; Ross A KNEPPER; Jan KŘETÍNSKÝ; Shelly LEVY-TZEDEK; Jamy LI; Todd D MURPHEY; Laurel D RIEK a Dorsa SADIGH. Formalizing and guaranteeing human-robot interaction. Communications of the ACM. New York, NY, USA: ACM, 2021, roč. 64, č. 9, s. 78-84. ISSN 0001-0782. Dostupné z: https://doi.org/10.1145/3433637.

HASHEMI, Vahid; Jan KŘETÍNSKÝ; Stefanie MOHR a Emmanouil SEFERIS. Gaussian-Based Runtime Detection of Out-of-distribution Inputs for Neural Networks. In Runtime Verification - 21st International Conference, RV 2021, Virtual Event, October 11-14, 2021, Proceedings. Springer, 2021, s. 254-264. ISBN 9783030884932. Dostupné z: https://doi.org/10.1007/978-3-030-88494-9_14.

WEININGER, Maximilian; Kush GROVER; Shruti MISRA a Jan KŘETÍNSKÝ. Guaranteed Trade-Offs in Dynamic Information Flow Tracking Games. In 2021 60th IEEE Conference on Decision and Control (CDC), Austin, TX, USA, December 14-17, 2021. IEEE, 2021, s. 3786-3793. ISBN 9781665436595. Dostupné z: https://doi.org/10.1109/CDC45484.2021.9683447.

KŘETÍNSKÝ, Jan. LTL-Constrained Steady-State Policy Synthesis. In Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, IJCAI 2021, Virtual Event / Montreal, Canada, 19-27 August 2021. 2021, s. 4104-4111. ISBN 9780999241196. Dostupné z: https://doi.org/10.24963/IJCAI.2021/565.

GROVER, Kush; Fernando S BARBOSA; Jana TŮMOVÁ a Jan KŘETÍNSKÝ. Semantic Abstraction-Guided Motion Planning for scLTL Missions in Unknown Environments. In Robotics: Science and Systems XVII, Virtual Event, July 12-16, 2021. 2021, s. 1-8. ISBN 9780992374778. Dostupné z: https://doi.org/10.15607/RSS.2021.XVII.090.

ESPARZA, Javier; Jan KŘETÍNSKÝ a Salomon SICKERT. A Unified Translation of Linear Temporal Logic to ω-Automata. Journal of the ACM. 2020, roč. 67, č. 6, s. 1-61. ISSN 0004-5411. Dostupné z: https://doi.org/10.1145/3417995.

ASHOK, Pranav; Krishnendu CHATTERJEE; Jan KŘETÍNSKÝ; Maximilian WEININGER a Tobias WINKLER. Approximating Values of Generalized-Reachability Stochastic Games. In LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020. ACM, 2020, s. 102-115. ISBN 9781450371049. Dostupné z: https://doi.org/10.1145/3373718.3394761.

D'ANTONI, Loris; Martin HELFRICH; Jan KŘETÍNSKÝ; Emanuel RAMNEANTU a Maximilian WEININGER. Automata Tutor v3. In Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. Springer, 2020, s. 3-14. ISBN 9783030532901. Dostupné z: https://doi.org/10.1007/978-3-030-53291-8_1.

KŘETÍNSKÝ, Jan; Emanuel RAMNEANTU; Alexander SLIVINSKIY a Maximilian WEININGER. Comparison of Algorithms for Simple Stochastic Games. In Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, Belgium, September 21-22, 2020. 2020, s. 131-148. ISSN 20752180. Dostupné z: https://doi.org/10.4204/EPTCS.326.9.

ASHOK, Pranav; Vahid HASHEMI; Jan KŘETÍNSKÝ a Stefanie MOHR. DeepAbstract: Neural Network Abstraction for Accelerating Verification. In Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings. Springer, 2020, s. 92-107. ISBN 9783030591519. Dostupné z: https://doi.org/10.1007/978-3-030-59152-6_5.

ASHOK, Pranav; Mathias JACKERMEIER; Pushpak JAGTAP; Jan KŘETÍNSKÝ; Maximilian WEININGER a Majid ZAMANI. dtControl: decision tree learning algorithms for controller representation. In HSCC '20: 23rd ACM International Conference on Hybrid Systems: Computation and Control, Sydney, New South Wales, Australia, April 21-24, 2020. ACM, 2020, s. 1-2. ISBN 9781450370189. Dostupné z: https://doi.org/10.1145/3365365.3383468.

ASHOK, Pranav; Mathias JACKERMEIER; Pushpak JAGTAP; Jan KŘETÍNSKÝ; Maximilian WEININGER a Majid ZAMANI. dtControl: decision tree learning algorithms for controller representation. In HSCC '20: 23rd ACM International Conference on Hybrid Systems: Computation and Control, Sydney, New South Wales, Australia, April 21-24, 2020. ACM, 2020, s. 1-7. ISBN 9781450370189. Dostupné z: https://doi.org/10.1145/3365365.3382220.

KŘETÍNSKÝ, Jan; Fabian MICHEL; Lukáš MICHEL a Guillermo A PÉREZ. Finite-Memory Near-Optimal Learning for Markov Decision Processes with Long-Run Average Reward. In Proceedings of the Thirty-Sixth Conference on Uncertainty in Artificial Intelligence, UAI 2020, virtual online, August 3-6, 2020. 2020, s. 1149-1158.

BENEŠ, Nikola; Uli FAHRENBERG; Jan KŘETÍNSKÝ; Axel LEGAY a Louis-Marie TRAONOUEZ. Logical vs. behavioural specifications. Information and computation. San Diego: Academic Press Inc Elsevier Science, 2020, roč. 271, č. 104487, s. 1-24. ISSN 0890-5401. Dostupné z: https://doi.org/10.1016/j.ic.2019.104487.

KŘETÍNSKÝ, Jan a Tobias MEGGENDORFER. Of Cores: A Partial-Exploration Framework for Markov Decision Processes. Logical Methods in Computer Science. Technical University of Braunschweig, 2020, roč. 16, č. 4, s. 1-31. ISSN 1860-5974.

BUDDE, Carlos E; Arnd HARTMANNS; Michaela KLAUCK; Jan KŘETÍNSKÝ; David PARKER; Tim QUATMANN; Andrea TURRINI a Zheng Hao ZHANG. On Correctness, Precision, and Performance in Quantitative Verification - QComp 2020 Competition Report. In Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part IV. Springer, 2020, s. 216-241. ISBN 9783030837228. Dostupné z: https://doi.org/10.1007/978-3-030-83723-5_15.

ČEŠKA, Milan; Calvin CHAU a Jan KŘETÍNSKÝ. SeQuaiA: A Scalable Tool for Semi-Quantitative Analysis of Chemical Reaction Networks. In Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I. Springer, 2020, s. 653-666. ISBN 9783030532871. Dostupné z: https://doi.org/10.1007/978-3-030-53288-8_32.

ASHOK, Pranav; Przemyslaw DACA; Jan KŘETÍNSKÝ a Maximilian WEININGER. Statistical Model Checking: Black or White? In Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part I. Springer, 2020, s. 331-349. ISBN 9783030613617. Dostupné z: https://doi.org/10.1007/978-3-030-61362-4_19.

EISENTRAUT, Julia a Jan KŘETÍNSKÝ. Expected Cost Analysis of Attack-Defense Trees. In Quantitative Evaluation of Systems, 16th International Conference, QEST 2019, Glasgow, UK, September 10-12, 2019, Proceedings. Springer, 2019, s. 203-221. ISBN 9783030302801. Dostupné z: https://doi.org/10.1007/978-3-030-30281-8_12.

KŘETÍNSKÝ, Jan a Tobias MEGGENDORFER. Of Cores: A Partial-Exploration Framework for Markov Decision Processes. Online. In 30th International Conference on Concurrency Theory (CONCUR 2019). Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2019, s. 1-17. ISBN 978-3-95977-121-4. Dostupné z: https://doi.org/10.4230/LIPIcs.CONCUR.2019.5.

ASHOK, Pranav; Jan KŘETÍNSKÝ a Maximilian WEININGER. PAC Statistical Model Checking for Markov Decision Processes and Stochastic Games. In Computer Aided Verification (CAV 2019). Cham: Springer, 2019, s. 497-519. ISBN 978-3-030-25539-8. Dostupné z: https://doi.org/10.1007/978-3-030-25540-4_29.

WEININGER, Maximilian; Tobias MEGGENDORFER a Jan KŘETÍNSKÝ. Satisfiability Bounds for ω-Regular Properties in Bounded-Parameter Markov Decision Processes. In 58th IEEE Conference on Decision and Control, CDC 2019, Nice, France, December 11-13, 2019. IEEE, 2019, s. 2284-2291. ISBN 9781728113982. Dostupné z: https://doi.org/10.1109/CDC40024.2019.9029460.

KŘETÍNSKÝ, Jan; Alexander MANTA a Tobias MEGGENDORFER. Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis. In Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. Springer, 2019, s. 404-422. ISBN 9783030317836. Dostupné z: https://doi.org/10.1007/978-3-030-31784-3_24.

ČEŠKA, Milan a Jan KŘETÍNSKÝ. Semi-quantitative Abstraction and Analysis of Chemical Reaction Networks. In Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I. Springer, 2019, s. 475-496. ISBN 9783030255398. Dostupné z: https://doi.org/10.1007/978-3-030-25540-4_28.

ČEŠKA, Milan a Jan KŘETÍNSKÝ. Semi-quantitative Abstraction and Analysis of Chemical Reaction Networks (Extended Abstract). In Computational Methods in Systems Biology - 17th International Conference, CMSB 2019, Trieste, Italy, September 18-20, 2019, Proceedings. Springer, 2019, s. 337-341. ISBN 9783030313036. Dostupné z: https://doi.org/10.1007/978-3-030-31304-3_22.

ASHOK, Pranav; Jan KŘETÍNSKÝ; Kim G. LARSEN; Adrien Le COËNT; Jakob Haahr TAANKVIST a Maximilian WEININGER. SOS: Safe, Optimal and Small Strategies for Hybrid Markov Decision Processes. In Quantitative Evaluation of Systems, 16th International Conference, QEST 2019, Glasgow, UK, September 10-12, 2019, Proceedings. Springer, 2019, s. 147-164. ISBN 9783030302801. Dostupné z: https://doi.org/10.1007/978-3-030-30281-8_9.

ASHOK, Pranav; Tomáš BRÁZDIL; Krishnendu CHATTERJEE; Jan KŘETÍNSKÝ; Christoph LAMPERT a Viktor TOMAN. Strategy Representation by Decision Trees with Linear Classifiers. In Quantitative Evaluation of Systems (QEST 2019). Cham: Springer, 2019, s. 109-128. ISBN 978-3-030-30280-1. Dostupné z: https://doi.org/10.1007/978-3-030-30281-8_7.

HAHN, Ernst Moritz; Arnd HARTMANNS; Christian HENSEL; Michaela KLAUCK; Joachim KLEIN; Jan KŘETÍNSKÝ; David PARKER; Tim QUATMANN; Enno RUIJTERS a Marcel STEINMETZ. The 2019 Comparison of Tools for the Analysis of Quantitative Formal Models - (QComp 2019 Competition Report). In Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III. Springer, 2019, s. 69-92. ISBN 9783030175016. Dostupné z: https://doi.org/10.1007/978-3-030-17502-3_5.

FAHRENBERG, Uli; Jan KŘETÍNSKÝ; Axel LEGAY a Louis-Marie TRAONOUEZ. Compositionality for quantitative specifications. Soft Computing. 2018, roč. 22, č. 4, s. 1139-1158. ISSN 1433-7479. Dostupné z: https://doi.org/10.1007/S00500-017-2519-5.

KŘETÍNSKÝ, Jan a Tobias MEGGENDORFER. Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes. Online. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18). New York, NY, USA: ACM, 2018, s. 609-618. ISBN 978-1-4503-5583-4. Dostupné z: https://doi.org/10.1145/3209108.3209176.

ASHOK, Pranav; Yuliya BUTKOVA; Holger HERMANNS a Jan KŘETÍNSKÝ. Continuous-Time Markov Decisions Based on Partial Exploration. In Automated Technology for Verification and Analysis. ATVA 2018. Cham: Springer, 2018, s. 317-334. ISBN 978-3-030-01089-8. Dostupné z: https://doi.org/10.1007/978-3-030-01090-4_19.

KŘETÍNSKÝ, Jan; Guillermo PEREZ a Jean-Francois RASKIN. Learning-Based Mean-Payoff Optimization in an Unknown MDP under Omega-Regular Constraints. Online. In 29th International Conference on Concurrency Theory (CONCUR 2018). Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2018, s. 1-18. ISBN 978-3-95977-087-3. Dostupné z: https://doi.org/10.4230/LIPIcs.CONCUR.2018.8.

ASHOK, Pranav; Tomáš BRÁZDIL; Jan KŘETÍNSKÝ a Ondřej SLÁMEČKA. Monte Carlo Tree Search for Verifying Reachability in Markov Decision Processes. In Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 2018). Cham: Springer, 2018, s. 322-335. ISBN 978-3-030-03420-7. Dostupné z: https://doi.org/10.1007/978-3-030-03421-4_21.

ESPARZA, Javier; Jan KŘETÍNSKÝ a Salomon SICKERT. One Theorem to Rule Them All: A Unified Translation of LTL into ω-Automata. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018. ACM, 2018, s. 384-393. ISBN 9781450355834. Dostupné z: https://doi.org/10.1145/3209108.3209161.

KŘETÍNSKÝ, Jan; Tobias MEGGENDORFER a Salomon SICKERT. Owl: A Library for ω-Words, Automata, and LTL. In Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings. Springer, 2018, s. 543-550. ISBN 9783030010898. Dostupné z: https://doi.org/10.1007/978-3-030-01090-4_34.

KŘETÍNSKÝ, Jan; Tobias MEGGENDORFER; Salomon SICKERT a Christopher ZIEGLER. Rabinizer 4: From LTL to Your Favourite Deterministic Automaton. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. Springer, 2018, s. 567-577. ISBN 9783319961446. Dostupné z: https://doi.org/10.1007/978-3-319-96145-3_30.

BRÁZDIL, Tomáš; Krishnendu CHATTERJEE; Jan KŘETÍNSKÝ a Viktor TOMAN. Strategy Representation by Decision Trees in Reactive Synthesis. In 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018). Cham: Springer, 2018, s. 385-407. ISBN 978-3-319-89959-6. Dostupné z: https://doi.org/10.1007/978-3-319-89960-2_21.

KŘETÍNSKÝ, Jan a Alexej ROTAR. The Satisfiability Problem for Unbounded Fragments of Probabilistic CTL. In 29th International Conference on Concurrency Theory, CONCUR 2018, September 4-7, 2018, Beijing, China. Dagstuhl, 2018, s. 1-16. ISBN 9783959770873. Dostupné z: https://doi.org/10.4230/LIPICS.CONCUR.2018.32.

KELMENDI, Edon; Julia KRÄMER; Jan KŘETÍNSKÝ a Maximilian WEININGER. Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm. In Computer Aided Verification (CAV 2018). Cham: Springer, 2018, s. 623-642. ISBN 978-3-319-96144-6. Dostupné z: https://doi.org/10.1007/978-3-319-96145-3_36.

KŘETÍNSKÝ, Jan a Tobias MEGGENDORFER. Efficient Strategy Iteration for Mean Payoff in Markov Decision Processes. In Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings. Springer, 2017, s. 380-399. ISBN 9783319681665. Dostupné z: https://doi.org/10.1007/978-3-319-68167-2_25.

DACA, Przemyslaw; Thomas A HENZINGER; Jan KŘETÍNSKÝ a Tatjana PETROV. Faster Statistical Model Checking for Unbounded Temporal Properties. ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. UNITED STATES: ASSOC COMPUTING MACHINERY, 2017, roč. 18, č. 2, s. 1-25. ISSN 1529-3785. Dostupné z: https://doi.org/10.1145/3060139.

ESPARZA, Javier; Jan KŘETÍNSKÝ; Jean-François RASKIN a Salomon SICKERT. From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I. Springer, 2017, s. 426-442. ISBN 9783662545768. Dostupné z: https://doi.org/10.1007/978-3-662-54577-5_25.

KŘETÍNSKÝ, Jan; Tobias MEGGENDORFER; Clara WALDMANN a Maximilian WEININGER. Index Appearance Record for Transforming Rabin Automata into Parity Automata. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I. Springer, 2017, s. 443-460. ISBN 9783662545768. Dostupné z: https://doi.org/10.1007/978-3-662-54577-5_26.

SVOREŇOVÁ, Mária; Jan KŘETÍNSKÝ; Martin CHMELÍK; Krishnendu CHATTERJEE; Ivana ČERNÁ a Calin BELTA. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. Elsevier, 2017, roč. 23, February 2017, s. 230-253. ISSN 1751-570X. Dostupné z: https://doi.org/10.1016/j.nahs.2016.04.006.

CHATTERJEE, Krishnendu; Zuzana KOMÁRKOVÁ a Jan KŘETÍNSKÝ. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. Logical Methods in Computer Science. Technical University of Braunschweig, 2017, roč. 13, č. 2, s. 1-50. ISSN 1860-5974. Dostupné z: https://doi.org/10.23638/LMCS-13(2:15)2017.

ASHOK, Pranav; Krishnendu CHATTERJEE; Przemyslaw DACA; Jan KŘETÍNSKÝ a Tobias MEGGENDORFER. Value Iteration for Long-Run Average Reward in Markov Decision Processes. In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. Springer, 2017, s. 201-221. ISBN 978-3-319-63386-2. Dostupné z: https://doi.org/10.1007/978-3-319-63387-9_10.

KŘETÍNSKÝ, Jan. 30 Years of Modal Transition Systems: Survey of Extensions and Analysis. In Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday. Springer, 2017, s. 36-74. ISSN 03029743. Dostupné z: https://doi.org/10.1007/978-3-319-63121-9_3.

DACA, Przemyslaw; Thomas A. HENZINGER; Jan KŘETÍNSKÝ a Tatjana PETROV. Faster Statistical Model Checking for Unbounded Temporal Properties. In Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016. Berlin Heidelberg: Springer, 2016, s. 112-129. ISBN 978-3-662-49673-2. Dostupné z: https://doi.org/10.1007/978-3-662-49674-9_7.

ESPARZA, Javier; Jan KŘETÍNSKÝ a Salomon SICKERT. From LTL to deterministic automata (A safraless compositional approach). Formal Methods in System Design. Springer Netherlands, 2016, roč. 49, č. 3, s. 219-271. ISSN 0925-9856. Dostupné z: https://doi.org/10.1007/s10703-016-0259-2.

SICKERT, Salomon; Javier ESPARZA; Stefan JAAX a Jan KŘETÍNSKÝ. Limit-Deterministic Büchi Automata for Linear Temporal Logic. In Computer Aided Verification - 28th International Conference, CAV 2016. Switzerland: Springer, 2016, s. 312-332. ISBN 978-3-319-41539-0. Dostupné z: https://doi.org/10.1007/978-3-319-41540-6_17.

DACA, Przemyslaw; Thomas A. HENZINGER; Jan KŘETÍNSKÝ a Tatjana PETROV. Linear Distances between Markov Chains. Online. In 27th International Conference on Concurrency Theory, CONCUR 2016. Schloss Dagstuhl: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016, s. 1-15. ISBN 978-3-95977-017-0. Dostupné z: https://doi.org/10.4230/LIPIcs.CONCUR.2016.20.

SICKERT, Salomon a Jan KŘETÍNSKÝ. MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata. In Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016. Switzerland: Springer, 2016, s. 130-137. ISBN 978-3-319-46519-7. Dostupné z: https://doi.org/10.1007/978-3-319-46520-3_9.

KŘETÍNSKÝ, Jan. Survey of Statistical Verification of Linear Unbounded Properties: Model Checking and Distances. In Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016. Switzerland: Springer, 2016, s. 27-45. ISBN 978-3-319-47165-5. Dostupné z: https://doi.org/10.1007/978-3-319-47166-2_3.

BENEŠ, Nikola; Przemysław DACA; Thomas A. HENZINGER; Jan KŘETÍNSKÝ a Dejan NIČKOVIĆ. Complete Composition Operators for IOCO-Testing Theory. Online. In Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering. New York, NY, USA: ACM, 2015, s. 101-110. ISBN 978-1-4503-3471-6. Dostupné z: https://doi.org/10.1145/2737166.2737175.

FAHRENBERG, Uli; Jan KŘETÍNSKÝ; Axel LEGAY a Louis-Marie TRAONOUEZ. Compositionality for Quantitative Specifications. In The 11th International Symposium on Formal Aspects of Component Software - FACS 2014. Heidelberg Dordrecht London New York: Springer, 2015, s. 306-324. ISBN 978-3-319-15316-2. Dostupné z: https://doi.org/10.1007/978-3-319-15317-9_19.

FOREJT, Vojtěch; Jan KRČÁL a Jan KŘETÍNSKÝ. Controller Synthesis for MDPs and Frequency LTL\GU. In LPAR 2015. Suva, Fiji: Springer, 2015, s. 162-177. ISBN 978-3-662-48898-0. Dostupné z: https://doi.org/10.1007/978-3-662-48899-7_12.

BRÁZDIL, Tomáš; Krishnendu CHATTERJEE; Martin CHMELÍK; Andreas FELLNER a Jan KŘETÍNSKÝ. Counterexample Explanation by Learning Small Strategies in Markov Decision Processes. In Daniel Kroening, Corina Pasareanu. Computer Aided Verification: 27th International Conference, CAV 2015. Cham: Springer, 2015, s. 158-177. ISBN 978-3-319-21689-8. Dostupné z: https://doi.org/10.1007/978-3-319-21690-4_10.

KŘETÍNSKÝ, Jan; Kim Guldstrand LARSEN; Simon LAURSEN a Jiří SRBA. Polynomial Time Decidability of Weighted Synchronization under Partial Observability. Online. In 26th International Conference on Concurrency Theory (CONCUR 2015). Dagstuhl, Germany: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015, s. 142-154. ISBN 978-3-939897-91-0. Dostupné z: https://doi.org/10.4230/LIPIcs.CONCUR.2015.142.

BENEŠ, Nikola; Jan KŘETÍNSKÝ; Kim G. LARSEN; Mikael H. MOLLER; Salomon SICKERT a Jiří SRBA. Refinement checking on parametric modal transition systems. Acta Informatica. Springer, 2015, roč. 52, 2-3, s. 269-297. ISSN 0001-5903. Dostupné z: https://doi.org/10.1007/s00236-015-0215-4.

SVOREŇOVÁ, Mária; Jan KŘETÍNSKÝ; Martin CHMELÍK; Krishnendu CHATTERJEE; Ivana ČERNÁ a Calin BELTA. Temporal Logic Control for Stochastic Linear Systems using Abstraction Refinement of Probabilistic Games. Online. In Proceedings of ACM international conference on Hybrid Systems: Computation and Control. Seattle, Washington, USA: Association for Computing Machinery (ACM), 2015, s. 259-268. ISBN 978-1-4503-3433-4. Dostupné z: https://doi.org/10.1145/2728606.2728608.

BABIAK, Tomáš; František BLAHOUDEK; Alexandre DURET-LUTZ; Joachim KLEIN; Jan KŘETÍNSKÝ; David MÜLLER; David PARKER a Jan STREJČEK. The Hanoi Omega-Automata Format. In Daniel Kroening, Corina Pasareanu. Computer Aided Verification: 27th International Conference, CAV 2015. Cham: Springer, 2015, s. 479-486. ISBN 978-3-319-21689-8. Dostupné z: https://doi.org/10.1007/978-3-319-21690-4_31.

CHATTERJEE, Krishnendu; Zuzana KOMÁRKOVÁ a Jan KŘETÍNSKÝ. Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes. In Thirtieth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Los Alamitos, California: IEEE, 2015, s. 244-256. ISBN 978-1-4799-8875-4. Dostupné z: https://doi.org/10.1109/LICS.2015.32.

ESPARZA, Javier a Jan KŘETÍNSKÝ. From LTL to Deterministic Automata: A Safraless Compositional Approach. In Computer Aided Verification - 26th International Conference, CAV 2014. Heidelberg Dordrecht London New York: Springer, 2014, s. 192-208. ISBN 978-3-319-08866-2. Dostupné z: https://doi.org/10.1007/978-3-319-08867-9_13.

HERMANNS, Holger; Jan KRČÁL a Jan KŘETÍNSKÝ. Probabilistic Bisimulation: Naturally on Distributions. In CONCUR 2014 - Concurrency Theory - 25th International Conference. Heidelberg Dordrecht London New York: Springer, 2014, s. 249-265. ISBN 978-3-662-44583-9. Dostupné z: https://doi.org/10.1007/978-3-662-44584-6_18.

KOMÁRKOVÁ, Zuzana a Jan KŘETÍNSKÝ. Rabinizer 3: Safraless Translation of LTL to Small Deterministic Automata. In Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014. Heidelberg Dordrecht London New York: Springer, 2014, s. 235-241. ISBN 978-3-319-11935-9. Dostupné z: https://doi.org/10.1007/978-3-319-11936-6_17.

BRÁZDIL, Tomáš; Krishnendu CHATTERJEE; Martin CHMELÍK; Vojtěch FOREJT; Jan KŘETÍNSKÝ; Marta KWIATKOWSKA; David PARKER a Mateusz UJMA. Verification of Markov Decision Processes using Learning Algorithms. In Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014. Heidelberg Dordrecht London New York: Springer, 2014, s. 98-114. ISBN 978-3-319-11935-9. Dostupné z: https://doi.org/10.1007/978-3-319-11936-6_8.

CHATTERJEE, Krishnendu; Andreas GAISER a Jan KŘETÍNSKÝ. Automata with Generalized Rabin Pairs for Probabilistic Model Checking and LTL Synthesis. In Computer Aided Verification - 25th International Conference, CAV 2013. Heidelberg Dordrecht London New York: Springer, 2013, s. 559-575. ISBN 978-3-642-39798-1. Dostupné z: https://doi.org/10.1007/978-3-642-39799-8_37.

HERMANNS, Holger; Jan KRČÁL a Jan KŘETÍNSKÝ. Compositional Verification and Optimization of Interactive Markov Chains. In CONCUR 2013 - Concurrency Theory - 24th International Conference. Heidelberg Dordrecht London New York: Springer, 2013, s. 364-379. ISBN 978-3-642-40183-1. Dostupné z: https://doi.org/10.1007/978-3-642-40184-8_26.

BRÁZDIL, Tomáš; Vojtěch FOREJT; Jan KRČÁL; Jan KŘETÍNSKÝ a Antonín KUČERA. Continuous-Time Stochastic Games with Time-Bounded Reachability. Information and Computation. Elsevier, 2013, roč. 224, č. 1, s. 46-70. ISSN 0890-5401. Dostupné z: https://doi.org/10.1016/j.ic.2013.01.001.

BENEŠ, Nikola; Benoit DELAHAYE; Uli FAHRENBERG; Jan KŘETÍNSKÝ a Axel LEGAY. Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory. In CONCUR 2013 - Concurrency Theory - 24th International Conference. Heidelberg Dordrecht London New York: Springer, 2013, s. 76-90. ISBN 978-3-642-40183-1. Dostupné z: https://doi.org/10.1007/978-3-642-40184-8_7.

KŘETÍNSKÝ, Jan a Salomon SICKERT. MoTraS: A Tool for Modal Transition Systems and Their Extensions. In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013. Heidelberg Dordrecht London New York: Springer, 2013, s. 487-491. ISBN 978-3-319-02443-1. Dostupné z: https://doi.org/10.1007/978-3-319-02444-8_41.

KŘETÍNSKÝ, Jan a Salomon SICKERT. On Refinements of Boolean and Parametric Modal Transition Systems. In Z. Liu, J. Woodcock, and H. Zhu. Theoretical Aspects of Computing - ICTAC 2013 - 10th International Colloquium. Heidelberg Dordrecht London New York: Springer, 2013, s. 213-230. ISBN 978-3-642-39717-2. Dostupné z: https://doi.org/10.1007/978-3-642-39718-9_13.

BRÁZDIL, Tomáš; Ľuboš KORENČIAK; Jan KRČÁL; Jan KŘETÍNSKÝ a Vojtěch ŘEHÁK. On time-average limits in deterministic and stochastic Petri nets. In ACM/SPEC International Conference on Performance Engineering, ICPE'13. New York: ACM, 2013, s. 421-422. ISBN 978-1-4503-1636-1. Dostupné z: https://doi.org/10.1145/2479871.2479936.

KŘETÍNSKÝ, Jan a Ruslan LEDESMA GARZA. Rabinizer 2: Small Deterministic Automata for LTL\GU. In Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013. Heidelberg Dordrecht London New York: Springer, 2013, s. 446-450. ISBN 978-3-319-02443-1. Dostupné z: https://doi.org/10.1007/978-3-319-02444-8_32.

KŘETÍNSKÝ, Jan a Javier ESPARZA. Deterministic Automata for the (F,G)-fragment of LTL. In Computer Aided Verification - 24th International Conference. Heidelberg Dordrecht London New York: Springer, 2012, s. 7-22. ISBN 978-3-642-31423-0. Dostupné z: https://doi.org/10.1007/978-3-642-31424-7_7.

BENEŠ, Nikola; Jan KŘETÍNSKÝ; Kim G. LARSEN; Mikael H. MOLLER a Jiří SRBA. Dual-Priced Modal Transition Systems with Time Durations. In LPAR-18 - Logic for Programming, Artificial Intelligence, and Reasoning: 18th International Conference. Heidelberg Dordrecht London New York: Springer, 2012, s. 122-137. ISBN 978-3-642-28716-9. Dostupné z: https://doi.org/10.1007/978-3-642-28717-6_12.

BENEŠ, Nikola; Jan KŘETÍNSKÝ; Kim G. LARSEN a Jiří SRBA. EXPTIME-Completeness of Thorough Refinement on Modal Transition Systems. Information and Computation. Elsevier, 2012, roč. 218, September, s. 54-68. ISSN 0890-5401. Dostupné z: https://doi.org/10.1016/j.ic.2012.08.001.

BENEŠ, Nikola a Jan KŘETÍNSKÝ. Modal Process Rewrite Systems. In Theoretical Aspects of Computing - ICTAC 2012. Berlin Heidelberg: Springer, 2012, s. 120-135. ISBN 978-3-642-32942-5. Dostupné z: https://doi.org/10.1007/978-3-642-32943-2_9.

GAISER, Andreas; Jan KŘETÍNSKÝ a Javier ESPARZA. Rabinizer: Small Deterministic Automata for LTL(F,G). In Automated Technology for Verification and Analysis - 10th International Symposium ATVA 2012. Berlin Heidelberg: Springer, 2012, s. 72-76. ISBN 978-3-642-33385-9. Dostupné z: https://doi.org/10.1007/978-3-642-33386-6_7.

BRÁZDIL, Tomáš; Holger HERMANNS; Jan KRČÁL; Jan KŘETÍNSKÝ a Vojtěch ŘEHÁK. Verification of Open Interactive Markov Chains. In Deepak D'Souza and Telikepalli Kavitha and Jaikumar Radhakrishnan. IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Dagstuhl, Germany: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2012, s. 474-485. ISBN 978-3-939897-47-7. Dostupné z: https://doi.org/10.4230/LIPIcs.FSTTCS.2012.474.

BRÁZDIL, Tomáš; Jan KRČÁL; Jan KŘETÍNSKÝ a Vojtěch ŘEHÁK. Fixed-delay Events in Generalized Semi-Markov Processes Revisited. In CONCUR 2011 - Concurrency Theory: 22nd International Conference. Berlin Heidelberg New York: Springer, 2011, s. 140-155. ISBN 978-3-642-23216-9.

BRÁZDIL, Tomáš; Jan KRČÁL; Jan KŘETÍNSKÝ; Antonín KUČERA a Vojtěch ŘEHÁK. Measuring Performance of Continuous-Time Stochastic Processes using Timed Automata. In Emilio Frazzoli, Radu Grosu. HSCC 11: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control. New York: ACM, 2011, s. 33-42. ISBN 978-1-4503-0629-4.

BENEŠ, Nikola; Ivana ČERNÁ a Jan KŘETÍNSKÝ. Modal Transition Systems: Composition and LTL Model Checking. In ATVA 2011 - Automated Technology for Verification and Analysis: 9th International Symposium. Heidelberg Dordrecht London New York: Springer, 2011, s. 228-242. ISBN 978-3-642-24371-4.

BENEŠ, Nikola; Jan KŘETÍNSKÝ; Kim G. LARSEN; Mikael H. MOLLER a Jiří SRBA. Parametric Modal Transition Systems. In ATVA 2011 - Automated Technology for Verification and Analysis: 9th International Symposium. Heidelberg Dordrecht London New York: Springer, 2011, s. 275-289. ISBN 978-3-642-24371-4.

BENEŠ, Nikola a Jan KŘETÍNSKÝ. Process Algebra for Modal Transition Systemses. Online. In Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers. Dagstuhl, Germany: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2011, s. 9--18. ISBN 978-3-939897-22-4.

BENEŠ, Nikola a Jan KŘETÍNSKÝ. Process Algebra for Modal Transition Systemses. In MEMICS 2010. Brno: NOVPRESS s.r.o., 2010, s. 20-27. ISBN 978-80-87342-10-7.

BRÁZDIL, Tomáš; Jan KRČÁL; Jan KŘETÍNSKÝ; Antonín KUČERA a Vojtěch ŘEHÁK. Stochastic Real-Time Games with Qualitative Timed Automata Objectives. In CONCUR 2010 - Concurrency Theory. Berlin Heidelberg New York: Springer, 2010, s. 207-221. ISBN 978-3-642-15374-7. Dostupné z: https://doi.org/10.1007/978-3-642-15375-4_15.

BRÁZDIL, Tomáš; Vojtěch FOREJT; Jan KRČÁL; Jan KŘETÍNSKÝ a Antonín KUČERA. Continuous-Time Stochastic Games with Time-Bounded Reachability. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2009). Dagstuhl, Germany: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2009, s. 61-72. ISBN 978-3-939897-13-2.

BENEŠ, Nikola; Jan KŘETÍNSKÝ; Kim G. LARSEN a Jiří SRBA. Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete. In Theoretical Aspects of Computing - ICTAC 2009, 6th International Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009. Proceedings. Heidelberg: Springer-Verlag, 2009, s. 112-126. ISBN 978-3-642-03465-7. Dostupné z: https://doi.org/10.1007/978-3-642-03466-4_7.

BENEŠ, Nikola; Jan KŘETÍNSKÝ; Kim G. LARSEN a Jiří SRBA. On Determinism in Modal Transition Systems. Theoretical Computer Science. Elsevier, 2009, roč. 410/2009, č. 41, s. 4026-4043. ISSN 0304-3975.

BRÁZDIL, Tomáš; Vojtěch FOREJT; Jan KŘETÍNSKÝ a Antonín KUČERA. The Satisfiability Problem for Probabilistic CTL. In 23rd IEEE Symposium on Logic in Computer Science (LICS 2008), 24-27 June 2008, Pittsburgh, USA, Proceedings. Los Alamitos, California: IEEE Computer Society, 2008, s. 391-402, 10 s. ISBN 978-0-7695-3183-0.