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