A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker, PRISM: A Tool for Automatic Verification of Probabilistic Systems, Proc. TACAS'06, ser. LNCS, 2006.
DOI : 10.1007/11691372_29

J. Katoen, E. Hahn, H. Hermanns, D. Jansen, and I. Zapreev, The ins and outs of the probabilistic model checker MRMC, Proc. QEST'09, 2009.

H. Hansson and B. Jonsson, A logic for reasoning about time and reliability, Formal Aspects of Computing, vol.2, issue.1, pp.512-535, 1994.
DOI : 10.1007/BF01211866
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.6154

H. Bohnenkamp, P. Van-der-stok, H. Hermanns, and F. Vaandrager, Cost-optimisation of the IPv4 Zeroconf protocol, Proc. IPDS'03, 2003.

M. Kwiatkowska, G. Norman, and D. Parker, Stochastic Model Checking, Formal Methods for the Design of Computer , Communication and Software Systems: Performance Evaluation (SFM'07), ser. LNCS, 2007.
DOI : 10.1007/978-3-540-72522-0_6

M. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, 1994.
DOI : 10.1002/9780470316887

C. Baier, B. Haverkort, H. Hermanns, and J. Katoen, Model-checking algorithms for continuous-time markov chains, IEEE Transactions on Software Engineering, vol.29, issue.6, pp.524-541, 2003.
DOI : 10.1109/TSE.2003.1205180

A. Aziz, K. Sanwal, V. Singhal, and R. Brayton, Verifying continuous time Markov chains, Proc. CAV'96, ser. LNCS, pp.269-276, 1996.
DOI : 10.1007/3-540-61474-5_75
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.3391

H. Jensen, Model checking probabilistic real time systems, Proc. 7th Nordic Workshop on Programming Theory, 1996.

D. Beauquier, On probabilistic timed automata, Theoretical Computer Science, vol.292, issue.1, pp.65-84, 2003.
DOI : 10.1016/S0304-3975(01)00215-8
URL : https://hal.archives-ouvertes.fr/hal-00005596

M. Kwiatkowska, G. Norman, R. Segala, and J. Sproston, Automatic verification of real-time systems with discrete probability distributions, Theoretical Computer Science, vol.282, issue.1, pp.101-150, 2002.
DOI : 10.1016/S0304-3975(01)00046-9

R. Alur and D. Dill, A theory of timed automata, Theoretical Computer Science, vol.126, issue.2, pp.183-235, 1994.
DOI : 10.1016/0304-3975(94)90010-8

M. Kwiatkowska, G. Norman, D. Parker, and J. Sproston, Performance analysis of probabilistic timed automata using digital clocks, pp.33-78, 2006.

A. Hartmanns and H. Hermanns, A Modest Approach to Checking Probabilistic Timed Automata, 2009 Sixth International Conference on the Quantitative Evaluation of Systems, 2009.
DOI : 10.1109/QEST.2009.41

M. Kwiatkowska, G. Norman, J. Sproston, and F. Wang, Symbolic model checking for probabilistic timed automata, Information and Computation, vol.205, issue.7, pp.1027-1077, 2007.
DOI : 10.1016/j.ic.2007.01.004
URL : http://doi.org/10.1016/j.ic.2007.01.004

M. Kwiatkowska, G. Norman, and D. Parker, Stochastic Games for Verification of Probabilistic Timed Automata, Proc. FORMATS'09, ser. LNCS, 2009.
DOI : 10.1007/s10703-005-1632-8
URL : https://hal.archives-ouvertes.fr/inria-00457923

J. Berendsen, D. Jansen, and F. Vaandrager, Fortuna: Model Checking Priced Probabilistic Timed Automata, 2010 Seventh International Conference on the Quantitative Evaluation of Systems, 2010.
DOI : 10.1109/QEST.2010.41

H. Hermanns, Interactive Markov Chains and the Quest for Quantified Quality, ser, LNCS, 2002.

H. Fecher, M. Leucker, and V. Wolf, Don???t Know in Probabilistic Systems, Proc. SPIN'06, ser. LNCS, 2006.
DOI : 10.1007/3-540-58468-4_190
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.278.6729

J. Katoen, D. Klink, M. Leucker, and V. Wolf, Threevalued abstraction for continuous-time Markov chains Reachability analysis of probabilistic systems by successive refinements, Proc. CAV'07, ser Proc. PAPM/PROBMIV'01, ser. LNCS, 2001.

M. Kwiatkowska, G. Norman, and D. Parker, Gamebased abstraction for Markov decision processes, Proc. QEST'06, 2006.

M. Kattenbelt, M. Kwiatkowska, G. Norman, and D. Parker, A game-based abstraction-refinement framework for??Markov decision processes, Formal Methods in System Design, vol.58, issue.1???2, 2010.
DOI : 10.1007/s10703-010-0097-6

B. Wachter and L. Zhang, Best Probabilistic Transformers, Proc. VMCAI'10, ser. LNCS, 2010.
DOI : 10.1007/978-3-642-11319-2_26
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.215.6864

M. Kwiatkowska, G. Norman, D. Parker, and H. Qu, Assume-Guarantee Verification for Probabilistic Systems, Proc. TACAS'10, ser. LNCS, 2010.
DOI : 10.1007/978-3-642-12002-2_3
URL : https://hal.archives-ouvertes.fr/inria-00458058

R. Segala, Modelling and verification of randomized distributed real time systems, 1995.

K. Etessami, M. Kwiatkowska, M. Vardi, and M. Yannakakis, Multi-objective model checking of Markov decision processes, LMCS, vol.4, issue.4, pp.1-21, 2008.

L. Feng, M. Kwiatkowska, and D. Parker, Compositional Verification of Probabilistic Systems Using Learning, 2010 Seventh International Conference on the Quantitative Evaluation of Systems, 2010.
DOI : 10.1109/QEST.2010.24
URL : https://hal.archives-ouvertes.fr/inria-00531203

J. Katoen, T. Kemna, I. Zapreev, and D. Jansen, Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking, Proc. TACAS'07, ser, 2007.
DOI : 10.1007/978-3-540-71209-1_9
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.93.3016

M. Kwiatkowska, G. Norman, and D. Parker, Symmetry Reduction for Probabilistic Model Checking, Proc. CAV'06, ser. LNCS, 2006.
DOI : 10.1007/11817963_23

P. D. Argenio and P. Niebert, Partial order reduction on concurrent probabilistic programs, QEST'04, 2004.

C. Baier, M. Groesser, and F. Ciesinski, Partial order reduction for probabilistic systems, First International Conference on the Quantitative Evaluation of Systems, 2004. QEST 2004. Proceedings., 2004.
DOI : 10.1109/QEST.2004.1348037

A. Miner and D. Parker, Symbolic Representations and Analysis of Large Probabilistic Systems, Validation of Stochastic Systems: A Guide to Current Research, ser. LNCS (Tutorial Volume), 2004.
DOI : 10.1007/978-3-540-24611-4_9

T. Hérault, R. Lassaigne, F. Magniette, and S. Peyronnet, Approximate Probabilistic Model Checking, Proc. VMCAI'04, ser. LNCS, 2004.
DOI : 10.1007/978-3-540-24622-0_8

H. Younes and R. Simmons, Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling, Proc. CAV'02, ser. LNCS, 2002.
DOI : 10.1007/3-540-45657-0_17

T. Han, J. Katoen, and B. Damman, Counterexample generation in probabilistic model checking, IEEE TSE, vol.35, issue.209, pp.241-257

M. Kwiatkowska, G. Norman, and D. Parker, A Framework for Verification of Software with Time and Probabilities, Proc. FORMATS'10, ser, 2010.
DOI : 10.1007/978-3-642-15297-9_4
URL : https://hal.archives-ouvertes.fr/hal-00767473

T. Han, J. Katoen, and A. Mereacre, Approximate Parameter Synthesis for Probabilistic Time-Bounded Reachability, 2008 Real-Time Systems Symposium, 2008.
DOI : 10.1109/RTSS.2008.19

E. M. Hahn, H. Hermanns, and L. Zhang, Probabilistic reachability for parametric Markov models, Proc. SPIN'09, ser. LNCS, 2009.
DOI : 10.1007/s10009-010-0146-x