P. A. Abdulla and B. Jonsson, Verifying Programs with Unreliable Channels, Information and Computation, vol.127, issue.2, pp.91-101, 1996.
DOI : 10.1006/inco.1996.0053
URL : https://doi.org/10.1006/inco.1996.0053

C. Baier, N. Bertrand, and P. Schnoebelen, Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness, Lecture Notes in Computer Science, vol.83, issue.5, pp.212-227, 2006.
DOI : 10.1007/978-3-540-24611-4_13

C. Baier, N. Bertrand, and P. Schnoebelen, Verifying nondeterministic probabilistic channel systems against ??-regular linear-time properties, ACM Transactions on Computational Logic, vol.9, issue.1, 2007.
DOI : 10.1145/1297658.1297663
URL : https://hal.archives-ouvertes.fr/inria-00424516

C. Baier, Principles of model checking, 2008.

C. Baier, J. Katoen, H. Hermanns, and V. Wolf, Comparative branching-time semantics for Markov chains, Information and Computation, vol.200, issue.2, pp.149-214, 2005.
DOI : 10.1016/j.ic.2005.03.001
URL : https://doi.org/10.1016/j.ic.2005.03.001

N. Bertrand and P. Schnoebelen, Computable fixpoints in well-structured symbolic model checking, Formal Methods in System Design, vol.21, issue.3, pp.233-267, 2013.
DOI : 10.1007/BFb0028736
URL : https://hal.archives-ouvertes.fr/hal-00906826

D. P. Bertsekas and J. Tsitsiklis, Neuro-dynamic programming, Athena Scientific Anthropological Field Studies, 1996.
DOI : 10.1007/0-306-48332-7_333

D. P. Bertsekas and J. N. Tsitsiklis, An Analysis of Stochastic Shortest Path Problems, Mathematics of Operations Research, vol.16, issue.3, pp.580-595, 1991.
DOI : 10.1287/moor.16.3.580
URL : http://www.mit.edu/people/dimitrib/Stochasticsp.pdf

A. L. Blum and J. C. Langford, Probabilistic Planning in the Graphplan Framework, pp.319-332, 2000.
DOI : 10.1007/10720246_25

A. Bohy, V. Bruyère, E. Filiot, N. Jin, and J. Raskin, Acacia+, a Tool for LTL Synthesis, Lecture Notes in Computer Science, vol.7358, pp.652-657, 2012.
DOI : 10.1007/978-3-642-31424-7_45
URL : https://hal.archives-ouvertes.fr/hal-01196263

A. Bohy, V. Bruyère, E. Filiot, and J. Raskin, Synthesis from LTL Specifications with Mean-Payoff Objectives, p.3539, 1210.
DOI : 10.1007/978-3-642-36742-7_12
URL : https://hal.archives-ouvertes.fr/hal-01196260

A. Bohy, V. Bruyère, E. Filiot, and J. Raskin, Synthesis from LTL Specifications with Mean-Payoff Objectives, Lecture Notes in Computer Science, vol.7795, pp.169-184, 2013.
DOI : 10.1007/978-3-642-36742-7_12
URL : https://hal.archives-ouvertes.fr/hal-01196260

A. Bohy, V. Bruyère, and J. Raskin, Symblicit algorithms for optimal strategy synthesis in monotonic Markov decision processes, Electronic Proceedings in Theoretical Computer Science, vol.4144, issue.5, pp.51-67, 2014.
DOI : 10.1007/11817963_5
URL : http://www.cassting-project.eu/wp-content/uploads/BBR-synt14.pdf

R. E. 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
URL : http://www.paradise.caltech.edu/cns188/Handouts/Bryant86.pdf

P. Buchholz, Exact and ordinary lumpability in finite Markov chains, Journal of Applied Probability, vol.1, issue.01, pp.59-75, 1994.
DOI : 10.1016/0166-5316(88)90031-4
URL : ftp://fbi-news.informatik.uni-dortmund.de/pub/ls04-info/papers/QM/1994_lumpa.ps.Z

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

K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh, QUASY: Quantitative Synthesis Tool, Lecture Notes in Computer Science. Lecture Notes in Computer Science, vol.158, issue.1-2, pp.267-271, 2011.
DOI : 10.1016/0304-3975(95)00188-3

E. M. Clarke and E. A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic, Logic of Programs, pp.52-71, 1981.
DOI : 10.1007/BFb0025774

L. De-alfaro, Computing Minimum and Maximum Reachability Times in Probabilistic Systems, Lecture Notes in Computer Science, vol.1664, pp.66-81, 1999.
DOI : 10.1007/3-540-48320-9_7

S. Derisavi, H. Hermanns, and W. H. Sanders, Optimal state-space lumping in Markov chains, Information Processing Letters, vol.87, issue.6, pp.309-315, 2003.
DOI : 10.1016/S0020-0190(03)00343-0
URL : http://www.crhc.uiuc.edu/PERFORM/Papers/USAN_papers/02DER01.pdf

L. Doyen and J. Raskin, Improved Algorithms for the Automata-Based Approach to Model-Checking, Lecture Notes in Computer Science, vol.4424, pp.451-465, 2007.
DOI : 10.1007/978-3-540-71209-1_34
URL : http://www.ulb.ac.be/di/ssd/cfv/TechReps/TechRep_CFV_2009_111.pdf

R. E. Fikes and N. J. Nilsson, Strips: A new approach to the application of theorem proving to problem solving, Artificial Intelligence, vol.2, issue.3-4, pp.189-208, 1972.
DOI : 10.1016/0004-3702(71)90010-5

J. Filar and K. Vrieze, Competitive Markov Decision Processes, 1997.
DOI : 10.1007/978-1-4612-4054-9

E. Filiot, N. Jin, and J. Raskin, Antichains and compositional algorithms for LTL synthesis, Formal Methods in System Design, vol.102, issue.4, pp.261-296, 2011.
DOI : 10.1007/978-3-540-78127-1_35
URL : https://hal.archives-ouvertes.fr/hal-01196265

A. Finkel, Decidability of the termination problem for completely specified protocols, Distributed Computing, vol.28, issue.4, pp.129-135, 1994.
DOI : 10.1007/BF02277857

A. Finkel and P. Schnoebelen, Well-structured transition systems everywhere!, Theoretical Computer Science, vol.256, issue.1-2, pp.63-92, 2001.
DOI : 10.1016/S0304-3975(00)00102-X
URL : https://doi.org/10.1016/s0304-3975(00)00102-x

M. Fujita, P. C. Mcgeer, J. C. Yang, and -. , Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Form, Formal Methods in System Design, vol.10, issue.2/3, pp.149-169, 1997.
DOI : 10.1023/A:1008647823331

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.1109/TSE.1986.6313045
URL : ftp://ftp.sics.se/pub/SICS-reports/Reports/SICS-R--90-13--SE.ps.Z

A. Hartmanns, Modest: a unified language for quantitative models, pp.44-51, 2012.

G. Higman, Ordering by Divisibility in Abstract Algebras, Proceedings of the London Mathematical Society, vol.3, issue.1, pp.326-336, 1952.
DOI : 10.1112/plms/s3-2.1.326

R. A. Howard, Dynamic Programming and Markov Processes, 1960.

D. N. Jansen, J. Katoen, M. Oldenkamp, M. Stoelinga, and I. S. Zapreev, How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison, Haifa Verification Conference, pp.69-85, 2007.
DOI : 10.1007/978-3-540-77966-7_9

J. Katoen, I. S. Zapreev, E. M. Hahn, H. Hermanns, and D. N. Jansen, The ins and outs of the probabilistic model checker MRMC, Performance Evaluation, vol.68, issue.2, pp.90-104, 2011.
DOI : 10.1016/j.peva.2010.04.001

J. G. Kemeny and J. L. Snell, Finite Markov Chains, 1960.

M. Z. Kwiatkowska, G. Norman, and D. Parker, PRISM 4.0: Verification of Probabilistic Real-Time Systems, Lecture Notes in Computer Science, vol.1, issue.1-2, pp.585-591, 2011.
DOI : 10.1007/3-540-45657-0_17
URL : https://hal.archives-ouvertes.fr/hal-00648035

K. G. Larsen and A. Skou, Bisimulation through probabilistic testing, Information and Computation, vol.94, issue.1, pp.1-28, 1991.
DOI : 10.1016/0890-5401(91)90030-6
URL : https://doi.org/10.1016/0890-5401(91)90030-6

S. M. Majercik and M. L. Littman, Maxplan: a new approach to probabilistic planning, pp.86-93, 1998.

J. K. Pachl, Protocol description and analysis based on a state transition model with channel expressions, PSTV, Proceedings of the IFIP WG6.1, pp.207-219, 1987.

R. Paige and R. E. Tarjan, Three Partition Refinement Algorithms, SIAM Journal on Computing, vol.16, issue.6, pp.973-989, 1987.
DOI : 10.1137/0216062

D. Parker, Personal communication, pp.2013-2024

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

S. J. Russell and P. Norvig, Artificial Intelligence: A Modern Approach, 1995.

A. F. Veinott, On Finding Optimal Policies in Discrete Dynamic Programming with No Discounting, The Annals of Mathematical Statistics, vol.37, issue.5, pp.1284-1294, 1966.
DOI : 10.1214/aoms/1177699272
URL : http://doi.org/10.1214/aoms/1177699272

V. Essen, C. Jobstmann, and B. , Synthesizing Efficient Controllers, Lecture Notes in Computer Science, vol.158, issue.1&2, pp.428-444, 2012.
DOI : 10.1016/0304-3975(95)00188-3

R. Wimmer, B. Braitling, B. Becker, E. M. Hahn, P. Crouzen et al., Symblicit Calculation of Long-Run Averages for Concurrent Probabilistic Systems, 2010 Seventh International Conference on the Quantitative Evaluation of Systems, pp.27-36, 2010.
DOI : 10.1109/QEST.2010.12

M. D. Wulf, L. Doyen, T. A. Henzinger, and J. Raskin, Antichains: A New Algorithm for Checking Universality of Finite Automata, Lecture Notes in Computer Science, vol.4144, pp.17-30, 2006.
DOI : 10.1007/11817963_5