I have been the leader of the Stochastic models group in the chair of Dependable Systems and Software at Saarland University from September 2013 to December 2015.

I now work for Google.

Before that, I studied PhD in the group of prof. Kučera at Masaryk University, Brno, Czech Republic.

My thesis: Formal Analysis of Discrete-Event Systems with Hard Real-Time Bounds

Areas of research

Formal methods, probabilistic verification, performance evaluation, game theory

Teaching

Quantitative Model Checking - winter 14/15

Contact

  • Address:
    Saarland University
    Department of Computer Science
    Campus Saarbrücken
    Bldg. E1 3, Room 534
    66123 Saarbrücken
  • Phone: +49 681 302 64092
  • E-mail: krcal@cs.uni-saarland.de

Publications

Can easily get outdated, a good approximation is on dblp.

  • Holger Hermanns, Jan Krcál, Jan Kretínský:
    Probabilistic Bisimulation: Naturally on Distributions. CONCUR 2014. PDF
  • Lubos Korenciak, Jan Krcál, Vojtech Rehák:
    Dealing with Zero Density Using Piecewise Phase-Type Approximation. EPEW 2014. PDF
  • Michal Abaffy, Tomás Brázdil, Vojtech Rehák, Branislav Bosanský, Antonín Kucera, Jan Krcál:
    Solving adversarial patrolling games with bounded error: (extended abstract). AAMAS 2014. PDF
  • Vahid Hashemi, Hassan Hatefi, Jan Krcál:
    Probabilistic Bisimulations for PCTL Model Checking of Interval MDPs. SynCoP 2014. PDF
  • Holger Hermanns, Jan Krcál, Jan Kretínský:
    Compositional Verification and Optimization of Interactive Markov Chains. CONCUR 2013. PDF
  • Tomás Brázdil, Lubos Korenciak, Jan Krcál, Jan Kretínský, Vojtech Rehák:
    On time-average limits in deterministic and stochastic petri nets. Poster paper. ICPE 2013. PDF
  • Tomás Brázdil, Vojtech Forejt, Jan Krcál, Jan Kretínský, Antonín Kucera:
    Continuous-time stochastic games with time-bounded reachability. Inf. Comput. 224: 46-70 (2013). PDF
  • Tomás Brázdil, Holger Hermanns, Jan Krcál, Jan Kretínský, Vojtech Rehák:
    Verification of Open Interactive Markov Chains. FSTTCS 2012. PDF
  • Tomáš Brázdil, Jan Krčál, Jan Křetínský, Vojtěch Řehák:
    Fixed-delay Events in Generalized Semi-Markov Processes Revisited. CONCUR 2011. PDF
  • Tomáš Brázdil, Jan Krčál, Jan Křetínský, Antonín Kučera, Vojtěch Řehák:
    Measuring Performance of Continuous-Time Stochastic Processes using Timed Automata. HSCC 2011. PDF
  • Tomáš Brázdil, Jan Krčál, Jan Křetínský, Antonín Kučera, Vojtěch Řehák:
    Stochastic Real-Time Games with Qualitative Timed Automata Objectives, CONCUR 2010. PDF
  • Tomáš Brázdil, Vojtěch Forejt, Jan Krčál, Jan Křetínský, Antonín Kučera:
    Continuous-Time Stochastic Games with Time-Bounded Reachability, FSTTCS 2009. PDF