I. Bahar, E. Frohm, C. Gaona, G. Hachtel, E. Macii et al., Algebraic decision diagrams and their applications. Formal Methods in System Design, pp.171-206, 1997.
DOI : 10.1109/iccad.1993.580054

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.2128

A. Bianco and L. De-alfaro, Model checking of probabilistic and nondeterministic systems, Proc. 15th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'95), volume 1026 of LNCS, pp.499-513, 1995.
DOI : 10.1007/3-540-60692-0_70

R. Bloem, H. Gabow, and F. Somenzi, An algorithm for strongly connected component analysis in n log n symbolic steps, Proc. 3rd International Conference on Formal Methods in Computer- Aided Design (FMCAD'00), pp.37-54, 2000.

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

R. Calinescu, C. Ghezzi, M. Kwiatkowska, and R. Mirandola, Self-adaptive software needs quantitative verification at runtime, Communications of the ACM, vol.55, issue.9, 2012.
DOI : 10.1145/2330667.2330686

R. Calinescu, L. Grunske, M. Kwiatkowska, R. Mirandola, and G. Tamburrelli, Dynamic QoS Management and Optimization in Service-Based Systems, IEEE Transactions on Software Engineering, vol.37, issue.3, pp.387-409, 2011.
DOI : 10.1109/TSE.2010.92

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

E. Clarke, M. Fujita, P. Mcgeer, K. Mcmillan, J. Yang et al., Multi-terminal binary decision diagrams: An efficient data structure for matrix representation. Formal Methods in System Design, pp.10149-169, 1997.

C. L. Conway, K. S. Namjoshi, D. Dams, and S. A. Edwards, Incremental algorithms for interprocedural analysis of safety properties, Proc. CAV'05, pp.449-461, 2005.

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

C. Daws, Symbolic and Parametric Model Checking of Discrete-Time Markov Chains, Proc. 1st Int Coll. Theoretical Aspects of Computing, pp.280-294, 2004.
DOI : 10.1007/978-3-540-31862-0_21

L. De-alfaro, Formal Verification of Probabilistic Systems, 1997.

L. Feng, M. Kwiatkowska, and D. Parker, Automated Learning of Probabilistic Assumptions for Compositional Reasoning, Proc. 14th International Conference on Fundamental Approaches to Software Engineering (FASE'11), pp.2-17, 2011.
DOI : 10.1007/978-3-642-19811-3_2

URL : https://hal.archives-ouvertes.fr/hal-00647067

A. Filieri, C. Ghezzi, A. Leva, and M. Maggio, Self-adaptive software meets control theory: A preliminary approach supporting reliability requirements, 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), pp.283-292, 2011.
DOI : 10.1109/ASE.2011.6100064

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

V. Forejt, M. Kwiatkowska, G. Norman, and D. Parker, Automated Verification Techniques for Probabilistic Systems, Formal Methods for Eternal Networked Software Systems (SFM'11), pp.53-113, 2011.
DOI : 10.1007/978-3-642-21455-4_3

URL : https://hal.archives-ouvertes.fr/hal-00648037

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. M. Hahn, T. Han, and L. Zhang, Synthesis for PCTL in Parametric Markov Decision Processes, Proc. 3rd NASA Formal Methods Symposium (NFM'11), 2011.
DOI : 10.1214/aoms/1177699369

E. M. Hahn, H. Hermanns, B. Wachter, and L. Zhang, PARAM: A Model Checker for Parametric Markov Models, Proc. 22nd International Conference on Computer Aided Verification (CAV'10), pp.660-664, 2010.
DOI : 10.1007/978-3-642-14295-6_56

URL : https://hal.archives-ouvertes.fr/hal-00650737

E. M. Hahn, H. Hermanns, and L. Zhang, Probabilistic reachability for parametric Markov models, Proc. 16th International SPIN Workshop, pp.88-106, 2009.

T. Han, J. Katoen, and A. Mereacre, Approximate parameter synthesis for probabilistic timebounded reachability, Proc. IEEE Real-Time Systems Symposium (RTSS 08), pp.173-182

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

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

J. Kemeny, J. Snell, and A. Knapp, Denumerable Markov Chains, 1976.
DOI : 10.1007/978-1-4684-9455-6

M. Kwiatkowska, G. Norman, and D. Parker, PRISM 4.0: Verification of Probabilistic Real-Time Systems, Proc. 23rd International Conference on Computer Aided Verification (CAV'11), pp.585-591, 2011.
DOI : 10.1007/3-540-45657-0_17

URL : https://hal.archives-ouvertes.fr/hal-00648035

M. Kwiatkowska, G. Norman, and D. Parker, Probabilistic verification of herman's selfstabilisation algorithm. Formal Aspects of Computing, 2012.

M. Kwiatkowska, G. Norman, and J. Sproston, Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol, Formal Aspects of Computing, vol.14, issue.3, pp.295-318, 2003.
DOI : 10.1007/s001650300007

M. Kwiatkowska, D. Parker, and H. Qu, Incremental quantitative verification for Markov decision processes, 2011 IEEE/IFIP 41st International Conference on Dependable Systems & Networks (DSN), pp.359-370, 2011.
DOI : 10.1109/DSN.2011.5958249

URL : https://hal.archives-ouvertes.fr/hal-00647057

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

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

V. Shmatikov, Probabilistic analysis of an anonymity system, Journal of Computer Security, vol.12, issue.3-4, pp.355-377, 2004.
DOI : 10.3233/JCS-2004-123-403

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

M. Stoelinga, Alea jacta est: Verification of probabilistic, real-time and parametric systems, 2002.

S. Stoller, E. Bartocci, J. Seyster, R. Grosu, K. Havelund et al., Runtime Verification with State Estimation, Proc. 2nd International Conference on Runtime Verification (RV'11), 2011.
DOI : 10.1007/978-3-642-29860-8_15

R. Tarjan, Depth-first search and linear graph algorithms, SIAM Journal on Computing, vol.136, pp.146-160, 1972.