@article{KNSS2002,
  author    = {Marta Z. Kwiatkowska and
               Gethin Norman and
               Roberto Segala and
               Jeremy Sproston},
  title     = {Automatic verification of real-time systems with discrete probability
               distributions},
  journal   = {Th. Comp. Sci.},
  volume    = {282},
  number    = {1}
}

@article{hoelzl2017mdp,
  author     = {Johannes H{\"o}lzl},
  title      = {Markov chains and {Markov} decision processes in {Isabelle/HOL}},
  journal    = {Journal of Automated Reasoning},
  doi        = {10.1007/s10817-016-9401-5},
  year       = {2017},
  publisher  = {Springer}
}

@inproceedings{PTA-ITP-2018,
author  = {Wimmer, Simon and H\"olzl, Johannes},
booktitle = {{ITP} 2018, Proceedings},
editor = {Avigad, Jeremy and Mahboubi, Assia},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title   = {{MDP + TA = PTA}: Probabilistic Timed Automata, Formalized},
year = {2018}
}