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

A. Bianco and L. De-alfaro, Model checking of probabilistic and nondeterministic systems, Proc. FSTTCS'95, ser. LNCS, 1995.
DOI : 10.1007/3-540-60692-0_70

M. Kwiatkowska, G. Norman, and D. Parker, PRISM 4.0: Verification of Probabilistic Real-Time Systems, Proc. CAV'11, ser, 2011.
DOI : 10.1007/3-540-45657-0_17
URL : https://hal.archives-ouvertes.fr/hal-00648035

R. Calinescu and M. Kwiatkowska, Using quantitative analysis to implement autonomic IT systems, 2009 IEEE 31st International Conference on Software Engineering, pp.100-110, 2009.
DOI : 10.1109/ICSE.2009.5070512
URL : https://hal.archives-ouvertes.fr/inria-00458053

A. Filieri, C. Ghezzi, and G. Tamburrelli, Run-time efficient probabilistic model checking, Proceeding of the 33rd international conference on Software engineering, ICSE '11, 2011.
DOI : 10.1145/1985793.1985840

F. Ciesinski, C. Baier, M. Größer, and J. Klein, Reduction Techniques for Model Checking Markov Decision Processes, 2008 Fifth International Conference on Quantitative Evaluation of Systems, pp.45-54, 2008.
DOI : 10.1109/QEST.2008.45

R. Tarjan, Depth-First Search and Linear Graph Algorithms, SIAM Journal on Computing, vol.1, issue.2, pp.146-160, 1972.
DOI : 10.1137/0201010
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.327.8418

R. Bloem, H. N. Gabow, and F. Somenzi, An algorithm for strongly connected component analysis in log symbolic steps, Proc. FMCAD'00, ser. LNCS, pp.37-54, 1954.

R. Gentilini, C. Piazza, and A. Policriti, Computing strongly connected components in a linear number of symbolic steps, Proc. SODA'03, pp.573-582, 2003.

E. Abrahám, N. Jansen, R. Wimmer, J. Katoen, and B. Becker, DTMC Model Checking by SCC Reduction, 2010 Seventh International Conference on the Quantitative Evaluation of Systems
DOI : 10.1109/QEST.2010.13

O. V. Sokolsky and S. A. Smolka, Incremental model checking in the modal mu-calculus, CAV 94, ser. LNCS, pp.351-363, 1994.
DOI : 10.1007/3-540-58179-0_67

C. L. Conway, K. S. Namjoshi, D. Dams, and S. A. Edwards, Incremental Algorithms for Inter-procedural Analysis of Safety Properties, Proc. CAV'05, ser. LNCS, pp.449-461, 2005.
DOI : 10.1007/11513988_45

K. Heljanko, T. Junttila, and T. Latvala, Incremental and Complete Bounded Model Checking for Full PLTL, CAV 05, ser. LNCS, pp.98-111, 2005.
DOI : 10.1007/11513988_10

A. Pnueli, The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp.46-57, 1977.
DOI : 10.1109/SFCS.1977.32

C. Courcoubetis and M. Yannakakis, The complexity of probabilistic verification, Journal of the ACM, vol.42, issue.4, 1995.
DOI : 10.1145/210332.210339

L. De-alfaro, Formal verification of probabilistic systems, 1997.

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

E. Nuutila and E. Soisalon-soininen, On finding the strongly connected components in a directed graph, Information Processing Letters, vol.49, issue.1, pp.9-14, 1994.
DOI : 10.1016/0020-0190(94)90047-7

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

M. Kwiatkowska, G. Norman, and R. Segala, Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM?, Proc. CAV'01, ser. LNCS, 2001.
DOI : 10.1007/3-540-44585-4_17

J. Aspnes and M. Herlihy, Fast randomized consensus using shared memory, Journal of Algorithms, vol.11, issue.3, 1990.
DOI : 10.1016/0196-6774(90)90021-6

M. Kwiatkowska, G. Norman, and J. Sproston, Probabilistic Model Checking of the IEEE 802.11 Wireless Local Area Network Protocol, Proc. PAPM/PROBMIV'02, ser. LNCS, pp.169-187, 2002.
DOI : 10.1007/3-540-45605-8_11

R. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, vol.35, issue.8, pp.677-691, 1986.
DOI : 10.1109/TC.1986.1676819

J. Burch, E. Clarke, K. Mcmillan, D. Dill, and J. Hwang, Symbolic model checking: 10/sup 20/ states and beyond, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pp.428-439, 1990.
DOI : 10.1109/LICS.1990.113767

M. Kwiatkowska, G. Norman, and J. Sproston, Probabilistic model checking of deadline properties in the IEEE 1394