2010
  Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Performance Evaluation and Model Checking Join Forces. Communications of the ACM, , 2010.
  Christel Baier, Lucia Cloth, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Performability Assessment by Model Checking of Markov Reward Models. Formal Methods in Systems Design, , 2010.

2008
 
Christel Baier, and Joost-Pieter Katoen. Principles of Model Checking, MIT Press, 2008.
 
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Reachability in continuous-time Markov reward decision processes. In Erich Graedel, Joerg Flum, and Thomas Wilke, editors, Logic and Automata: History and Perspectives. pages 53–72. Volume 2 of Texts in Logics and Games. Amsterdam University Press, 2008.

2005
  Christel Baier, Joost-Pieter Katoen, Holger Hermanns, and Verena Wolf. Comparative branching-time semantics for Markov chains. Information and Computation, 200(2):149–214, 2005.
 
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Model checking meets performance evaluation. SIGMETRICS Performance Evaluation Review, 32(4):10–15, 2005.
  Christel Baier, Holger Hermanns, Joost-Pieter Katoen, and Boudewijn R. Haverkort. Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theoretical Computer Science, 345(1):2–26, 2005.

2004
  Christel Baier, Holger Hermanns, and Joost-Pieter Katoen. Probabilistic weak simulation is decidable in polynomial time. Information Processing Letters, 89(3):123–130, 2004.
  Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen, and Markus Siegle. Validation of Stochastic Systems. Lecture Notes in Computer Science, 465 pages, 2925, 2004.
  Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Efficient computation of maximal timed reachability probabilities in uniform continuous-time Markov decision processes. In K. Jensen, and A. Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pages 61–76. LNCS vol. 2988, Springer-Verlag, 2004.

2003
  Christel Baier, Holger Hermanns, Joost-Pieter Katoen, and Verena Wolf. Comparative branching-time semantics for Markov chains. In Roberto M. Amadio, and Denis Lugiez, editors, Concurrency Theory (CONCUR). pages 492–508. LNCS vol. 2761, Springer-Verlag, 2003.
  Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering, 29(6):524–541, 2003.

2002
  Boudewijn R. Haverkort, Lucia Cloth, Holger Hermanns, Joost-Pieter Katoen, and Christel Baier. Model checking performability properties. In Dependable Systems and Networks (DSN). pages 103–113. IEEE CS Press, 2002.
  Christel Baier, Joost-Pieter Katoen, Holger Hermanns, and Boudewijn R. Haverkort. Simulation for continuous-time Markov chains. In Lubos Brim, Petr Jancar, Mojmír Kretínský, and Antonín Kucera, editors, Concurrency Theory (CONCUR). pages 338–354. LNCS vol. 2421, Springer-Verlag, 2002.
  Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Automated performance and dependability evaluation using model checking. In Mariacarla Calzarossa, and Salvatore Tucci, editors, Computer Performance Evaluation. pages 261–289. LNCS vol. 2459, Springer-Verlag, 2002.

2001
  Joost-Pieter Katoen, Christel Baier, and Diego Latella. Metric semantics for true concurrent real time. Theor. Comput. Sci, 254(1-2):501–542, 2001.

2000
  Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. On the logical characterisation of performability properties. In Ugo Montanari, José D.P. Rolim, and Emo Welzl, editors, Automata, Languages and Programming (ICALP). pages 780–792. LNCS vol. 1853, Springer-Verlag, 2000.
  Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Model checking continuous-time Markov chains by transient analysis. In Allen E. Emerson, and Prasad A. Sistla, editors, Computer-Aided Verification (CAV). pages 358–372. LNCS vol. 1855, Springer, 2000.

1999
  Christel Baier, Joost-Pieter Katoen, and Holger Hermanns. Approximate Symbolic Model Checking of Continuous-Time Markov Chains. In Jos C.M. Baeten, and Sjouke Mauw, editors, Concurrency Theory (CONCUR), volume 1664 of Lecture Notes in Computer Science, pages. pages 146–162. Springer, 1999.

1998
  Christel Baier, Joost-Pieter Katoen, and Diego Latella. Metric Semantics for True Concurrent Real Time. In Kim G. Larsen, S. Skyum, and G. Winskel, editors, Automata, Languages, and Programming (ICALP), volume 1443 of Lecture Notes in Computer Science. pages 568–580. Springer, 1998.