Go to main content | Go to main menu | Go to search

prof. Dr. rer. nat. RNDr. Mgr. Bc. Jan Křetínský, Ph.D.

Professor, Department of Computer Science

Office: C514
Botanická 554/68a
602 00 Brno

Show on the map

Phone: +420 549 49 4085
E‑mail:
social and academic networks:
Basic information
CV

Curriculum Vitae

Person-Related Identification Information
  • Jan Křetínský
    born 26/12/1984 in Brno
Department
  • Faculty of Informatics, Masaryk University
    Botanická 68a, Brno 602 00
Education and Academic Qualifications
  • 2011: RNDr. degree, Informatics - Parallel and Distributed Systems, Probabilistic Timed Systems with Non-Determinism, Faculty of Informatics, Masaryk University
  • 2010: Master's degree, Mathematics - Algebra and Discrete Mathematics, Modal Transition Systems, Faculty of Science, Masaryk University
  • 2009: Master's degree, Informatics - Parallel and Distributed Systems, Fundamental Properties of Probabilistic Branching-Time Logics, Faculty of Informatics, Masaryk University
  • 2007: Bachelor's degree, Mathematics - Mathematics, Monadic Second Order Logic on Infinite Words and Trees, Faculty of Science, Masaryk University
  • 2007: Bachelor's degree, Humanities - Philosophy, General Linguistics, Mathematical Framework for Natural Language Formal Description, Faculty of Arts, Masaryk University
  • 2007: Bachelor's degree, Informatics - Informatics, Use-mention Distinction in Transparent Intensional Logic, Faculty of Informatics, Masaryk University
Teaching Activities
  • Diskrete Wahrscheinlichkeitstheorie TUM (Summer 2012)
  • Complexity TUM (Summer 2010, 2011)
  • Automata and Formal Languages TUM (Winter 2009/10, 2010/11, 2011/12, 2012/13)
  • Complexity TUM (Summer 2010)
  • IA008 Computational Logic FI (Spring 2009)
  • IB102 Automata and Grammars FI (Autumn 2007)
  • MB003 Linear Algebra and Geometry I FI (Spring 2008)
  • MB005 Foundations of mathematics FI (Autumn 2007)
  • M1110 Linear Algebra and Geometry I PřF (Autumn 2007)
  • Students:
  • Carlos Camino: Probabilistic Cellular Automata
  • Moritz Fuchs: An Advanced Solver for Presburger Arithmetic
  • Martin Stoll: MoTraS: A Tool for Modal Transition Systems
  • Salomon Sickert: Refinement Algorithms for Parametric Modal Transition Systems
  • Imre Vadász: Discretization of Time-Bounded Reachability in Generalized Semi-Markov Games
  • Dennis Kraft: Almost Sure Winning Strategies in Stochastic Real Time Games with Timed Automata Objectives
  • Markus Dausch: Tool for Continuous Time Stochastic Games (GUI and Simulations)
  • Tuan Duc Nguyen: An Extension of a Tool for Modal Transition Systems
  • Philip Meyer: Algorithms for Refinement of Modal Process Rewrite Systems
  • Alexander Manta
  • Michael Opitz
Scientific and Research Activities
  • continuous-time stochastic processes and games; CoTtaGe (under development) - algorithms for continuous-time stochastic games and their extensions
  • temporal logics, in particular LTL and PCTL; Rabinizer 2 (developed with Ruslan Ledesma Garza), and Rabinizer (developed with Andreas Gaiser) - translation of LTL formulae to deterministic Rabin automata
  • modal transition systems; MoTraS (developed with Salomon Sickert), and the old version (developed with Martin Stoll) - algorithms for modal transition systems and their extensions
Academic Stays
Awards Related to Science and Research
  • 2009: Rector's Prize
  • 2007: Dean's Prize
Major Publications
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. URL info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info
  • 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. info

2013/06/20

Supervision
Qualifications
Publications
Projects
Teaching

You are running an old browser version. We recommend updating your browser to its latest version.

More info