Výpis publikací

DORFHUBER, Florian Sebastian, Julia EISENTRAUT, Katharina KLIOBA a Jan KŘETÍNSKÝ. QuADTool: Attack-Defense-Tree Synthesis, Analysis and Bridge to Verification. Online. QEST 2024: Springer, 2024. Dostupné z: https://dx.doi.org/15605.

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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.doi.org/10.1007/978-3-031-45329-8_19.

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://dx.doi.org/10.1007/978-3-031-22337-2_18.

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://dx.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. 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://dx.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://dx.doi.org/10.1007/978-3-030-25540-4_29.

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://dx.doi.org/10.1007/978-3-030-30281-8_7.

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://dx.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://dx.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://dx.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://dx.doi.org/10.1007/978-3-030-03421-4_21.

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://dx.doi.org/10.1007/978-3-319-89960-2_21.

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://dx.doi.org/10.1007/978-3-319-96145-3_36.

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://dx.doi.org/10.1016/j.nahs.2016.04.006.

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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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://dx.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.