. Scalability, A variety of approaches are being considered to improve scalability One example is the development of abstraction and refinement frameworks63], some of which have been applied in practice to verification of probabilistic timed automata [68], probabilistic software [62] and PRISM models [50]. Other promising directions include: partial order reduction [49,31], symmetry reduction [66,39], algorithms for simulation and bisimulation relations, p.38

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

L. De-alfaro, From Fairness to Chance, Proc. 1st Int. Workshop Probabilistic Methods in Verification (PROBMIV'98). ENTCS, 1998.
DOI : 10.1016/S1571-0661(05)80597-3

H. Aljazzar and S. Leue, Generation of Counterexamples for Model Checking of Markov Decision Processes, 2009 Sixth International Conference on the Quantitative Evaluation of Systems, pp.197-206, 2009.
DOI : 10.1109/QEST.2009.10

M. Andrés, P. D-'argenio, and P. Van-rossum, Significant Diagnostic Counterexamples in Probabilistic Model Checking, Proc. 4th Int. Haifa Verification Conf. Hardware and Software: Verification and Testing (HVC'08)
DOI : 10.1007/978-3-540-24611-4_1

J. Aspnes and M. Herlihy, Fast randomized consensus using shared memory, Journal of Algorithms, vol.11, issue.3, pp.441-460, 1990.
DOI : 10.1016/0196-6774(90)90021-6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.23.8873

A. Aziz, V. Singhal, F. Balarin, R. Brayton, and A. Sangiovanni-vincentelli, It usually works: The temporal logic of stochastic systems, Proc. 7th Int. Conf. Computer Aided Verification (CAV'95). LNCS, pp.155-165, 1995.
DOI : 10.1007/3-540-60045-0_48

C. Baier, On algorithmic verification methods for probabilistic systems, 1998.

C. Baier, M. Größer, and F. Ciesinski, Quantitative Analysis under Fairness Constraints, Proc. 7th Int. Symp. Automated Technology for Verification and Analysis (ATVA'09), pp.135-150, 2009.
DOI : 10.1007/978-3-642-04761-9_12

C. Baier, M. Größer, M. Leucker, B. Bollig, and F. Ciesinski, Controller synthesis for probabilistic systems, Proc. 3rd IFIP Int. Conf. Theoretical Computer Science (TCS'06, pp.493-5062, 2004.

C. Baier, H. Hermanns, J. P. Katoen, and B. Haverkort, Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes, Theoretical Computer Science, vol.345, issue.1, pp.2-26, 2005.
DOI : 10.1016/j.tcs.2005.07.022

C. Baier and J. P. Katoen, Principles of Model Checking, 2008.

C. Baier and M. Kwiatkowska, Model checking for a probabilistic branching time logic with fairness, Distributed Computing, vol.11, issue.3, pp.125-155, 1998.
DOI : 10.1007/s004460050046

J. Barnat, L. Brim, I. Cerna, M. Ceska, and J. Tumova, ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems, 2008 Fifth International Conference on Quantitative Evaluation of Systems, pp.77-78, 2008.
DOI : 10.1109/QEST.2008.29
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.406.3801

R. Bellman, Dynamic Programming, 1957.

L. Benini, A. Bogliolo, G. Paleologo, and G. De-micheli, Policy optimization for dynamic power management, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol.18, issue.6, pp.299-316, 2000.
DOI : 10.1109/43.766730
URL : http://akebono.stanford.edu/users/nanni/research/dpm/dac98.pdf

D. Bertsekas, Dynamic Programming and Optimal Control, Volumes 1 and 2, Athena Scientific, 1995.

D. Bertsekas and J. 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

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

T. Brázdil, V. Forejt, A. Ku?era, L. Aceto, I. Damgård et al., Controller Synthesis and Verification for Markov Decision Processes with Qualitative Branching Time Objectives, Proc. 35th Int. Colloq. Automata, Languages and Programming, Part II (ICALP'08). LNCS, pp.148-159, 2008.
DOI : 10.1007/978-3-540-70583-3_13

T. Brázdil, V. Bro?ek, V. Forejt, and A. Ku?era, Stochastic games with branchingtime winning objectives, 21th IEEE Symp. Logic in Computer Science, pp.349-358, 2006.

T. Brázdil, V. Bro?ek, A. Ku?era, and J. Obdr?álek, Qualitative reachability in stochastic BPA games, 26th Int. Symp. Theoretical Aspects of Computer Science (STACS'09). LIPIcs Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.207-218, 2009.
DOI : 10.1016/j.ic.2011.02.002

T. Brázdil, V. Forejt, J. Kr?ál, J. K?etínsk´k?etínsk´y, and A. Ku?era, Continuous-time stochastic games with time-bounded reachability, Proc. 29th Int. Conf. Foundations of Software Technology and Theoretical Computer Science (FSTTCS'09). LIPIcs, pp.61-72, 2009.
DOI : 10.1016/j.ic.2013.01.001

R. Calinescu, L. Grunske, M. Kwiatkowska, R. Mirandola, and G. Tamburrelli, Dynamic QoS management and optimisation in service-based systems, IEEE Transactions on Software Engineering, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00663216

S. Cattani, R. Segala, L. Brim, P. Janar, M. Ketinsky et al., Decision Algorithms for Probabilistic Bisimulation*, Proc. 14th Int. Conf. Concurrency Theory (CONCUR'02), pp.371-385, 2002.
DOI : 10.1007/3-540-45694-5_25
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.4.589

R. Chadha and M. Viswanathan, A counterexample-guided abstraction-refinement framework for markov decision processes, ACM Transactions on Computational Logic, vol.12, issue.1, pp.1-49, 2010.
DOI : 10.1145/1838552.1838553
URL : http://arxiv.org/abs/0807.1173

K. Chatterjee and T. Henzinger, Value Iteration, 25 Years of Model Checking -History, Achievements, Perspectives. LNCS, pp.107-138, 2008.
DOI : 10.1007/978-3-540-69850-0_7

K. Chatterjee, T. Henzinger, B. Jobstmann, and R. Singh, Measuring and synthesizing systems in probabilistic environments, Proc. 22nd Int. Conf. Computer Aided Verification (CAV'10), pp.380-395, 2010.

L. Cheung, Reconciling Nondeterministic and Probabilistic Choices, 2006.

F. Ciesinski and C. Baier, Liquor: A tool for qualitative and quantitative linear time analysis of reactive systems, Proc. 3rd Int. Conf. Quantitative Evaluation of Systems (QEST'06, pp.131-132, 2006.

F. Ciesinski, C. Baier, M. Größer, and D. Parker, 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

F. Ciesinski and M. Größer, On Probabilistic Computation Tree Logic, Validation of Stochastic Systems: A Guide to Current Research, pp.147-188, 2004.
DOI : 10.1007/978-3-540-24611-4_5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.141.6916

E. Clarke and A. Emerson, Design and synthesis of synchronization skeletons using branching time temporal logic, Proc. Workshop Logic of Programs, pp.52-71, 1981.

C. Courcoubetis and M. Yannakakis, Verifying temporal properties of finite-state probabilistic programs, [Proceedings 1988] 29th Annual Symposium on Foundations of Computer Science, pp.338-345, 1988.
DOI : 10.1109/SFCS.1988.21950

C. Courcoubetis and M. Yannakakis, Markov decision processes and regular events, IEEE Transactions on Automatic Control, vol.43, issue.10, pp.1399-1418, 1998.
DOI : 10.1109/9.720497

M. Daniele, F. Giunchiglia, and M. Vardi, Improved Automata Generation for Linear Temporal Logic, Proc. 11th Int. Conf. Computer Aided Verification (CAV'99), pp.249-260, 1999.
DOI : 10.1007/3-540-48683-6_23

D. 'argenio, P. Jeannet, B. Jensen, H. Larsen, and K. , Reduction and refinement strategies for probabilistic analysis, Proc. 2nd Joint Int. Workshop Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM/PROBMIV'02). LNCS, pp.57-76

B. Delahaye, B. Caillaud, and A. Legay, Probabilistic Contracts: A Compositional Reasoning Methodology for the Design of Stochastic Systems, 2010 10th International Conference on Application of Concurrency to System Design
DOI : 10.1109/ACSD.2010.13
URL : https://hal.archives-ouvertes.fr/inria-00554297

. Conf, Application of Concurrency to System Design (ACSD'10), pp.223-232, 2010.

A. Donaldson and A. Miller, Symmetry reduction for probabilistic model checking using generic representatives Automated Technology for Verification and Analysis (ATVA'06), Proc. 4th Int. Symp, pp.9-23, 2006.

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

K. Etessami, M. Yannakakis, L. Caires, G. Italiano, L. Monteiro et al., Recursive Markov decision processes and recursive stochastic games, Proc. 32nd Int. Colloq. Automata, Languages and Programming (ICALP'05), pp.891-903, 2005.
DOI : 10.1007/11523468_72
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.5131

W. Feller, An Introduction to Probability Theory and its Applications, 1968.

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

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, D. Parker, and H. Qu, Quantitative multiobjective verification for probabilistic systems, Proc. 17th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'11), pp.112-127, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00647055

M. Fränzle, T. Teige, and A. Eggers, Engineering constraint solvers for automatic analysis of probabilistic hybrid automata, The Journal of Logic and Algebraic Programming, vol.79, issue.7, pp.436-466, 2010.
DOI : 10.1016/j.jlap.2010.07.003

S. Giro, On the automatic verification of distributed probabilistic automata with partial information, 2010.

R. Van-glabbeek, S. Smolka, and B. Steffen, Reactive, generative, and stratified models of probabilistic processes, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pp.59-80, 1995.
DOI : 10.1109/LICS.1990.113740

M. Größer and C. Baier, Partial Order Reduction for Markov Decision Processes: A Survey, Proc. 4th Int. Symp. Formal Methods for Component and Objects (FMCO'05), pp.408-427, 2006.
DOI : 10.1007/11804192_19

E. Hahn, H. Hermanns, B. Wachter, and L. Zhang, PASS: Abstraction Refinement for Infinite Probabilistic Models, Proc. 16th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'10), pp.353-357, 2010.
DOI : 10.1007/978-3-642-12002-2_30

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

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

H. Hansson, Time and Probability in Formal Design of Distributed Systems, 1994.

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. Hinton, M. Kwiatkowska, G. Norman, and D. Parker, PRISM: A Tool for Automatic Verification of Probabilistic Systems
DOI : 10.1007/11691372_29

R. Howard, Dynamic Programming and Markov Processes Technical specifications of hard drive IBM Travelstar, 1960.

A. Israeli and M. Jalfon, Token management schemes and random walks yield selfstabilizating mutual exclusion, Proc. 9th Annual ACM Symp. Principles of Distributed Computing (PODC'90, pp.119-131, 1990.
DOI : 10.1145/93385.93409

B. Jeannet, P. D-'argenio, and K. Larsen, Rapture: A tool for verifying Markov decision processes, Proc. Tools Day, affiliated to 13th Int. Conf. Concurrency Theory (CONCUR'02, pp.84-98, 2002.

J. P. Katoen, E. Hahn, H. Hermanns, D. Jansen, and I. Zapreev, The ins and outs of the probabilistic model checker MRMC, Proc. 6th Int. Conf. Quantitative Evaluation of Systems (QEST'09, pp.167-176, 2009.

M. Kattenbelt, M. Kwiatkowska, G. Norman, and D. Parker, Abstraction Refinement for Probabilistic Software, Proc. 10th Int. Conf. Verification, Model Checking, and Abstract Interpretation (VMCAI'09), pp.182-197, 2009.
DOI : 10.1007/978-3-540-93900-9_17
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.431.3875

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

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

V. Kulkarni, Modeling and Analysis of Stochastic Systems, 1995.

M. Kwiatkowska, G. Norman, and D. Parker, Symmetry Reduction for Probabilistic Model Checking, Proc. 18th Int. Conf. Computer Aided Verification (CAV'06), pp.234-248, 2006.
DOI : 10.1007/11817963_23

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). LNCS (Tutorial Volume), pp.220-270, 2007.
DOI : 10.1007/978-3-540-72522-0_6

M. Kwiatkowska, G. Norman, and D. Parker, Stochastic Games for Verification of Probabilistic Timed Automata, Proc. 7th Int. Conf. Formal Modelling and Analysis of Timed Systems (FORMATS'09), pp.212-227, 2009.
DOI : 10.1007/s10703-005-1632-8
URL : https://hal.archives-ouvertes.fr/inria-00457923

M. Kwiatkowska, G. Norman, D. Parker, and H. Qu, Assume-Guarantee Verification for Probabilistic Systems, Proc. 16th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'10)
DOI : 10.1007/978-3-642-12002-2_3
URL : https://hal.archives-ouvertes.fr/inria-00458058

M. Kwiatkowska, G. Norman, D. Parker, and J. Sproston, Modeling and Verification of Real-Time Systems: Formalisms and Software Tools, chap. Verification of Real- Time Probabilistic Systems, pp.249-288, 2008.

M. Kwiatkowska, G. Norman, and R. Segala, Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM?, Proc. 13th Int. Conf. Computer Aided Verification (CAV'01), pp.194-206, 2001.
DOI : 10.1007/3-540-44585-4_17

A. Legay, A. Murawski, J. Ouaknine, and J. Worrell, On Automated Verification of Probabilistic Programs, Proc. 14th Int. Conf
DOI : 10.1007/978-3-540-78800-3_13

. Forejt and N. Kwiatkowska, Parker Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08)

M. Neuhäußer and L. Zhang, Time-bounded reachability probabilities in continuoustime Markov decision processes, Proc. 7th Int. Conf. Quantitative Evaluation of Systems (QEST'10, pp.209-218, 2010.

G. Norman, D. Parker, M. Kwiatkowska, S. Shukla, and R. Gupta, Using probabilistic model checking for dynamic power management, Formal Aspects of Computing, vol.17, issue.2, pp.160-176, 2005.
DOI : 10.1007/s00165-005-0062-0

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

M. Rabe and S. Schewe, Optimal Time-Abstract Schedulers for CTMDPs and Markov Games, Proc. 8th Workshop Quantitative Aspects of Programming Languages, pp.144-158, 2010.
DOI : 10.4204/EPTCS.28.10

M. Rabin, Probabilistic automata, Information and Control, vol.6, issue.3, pp.230-245, 1963.
DOI : 10.1016/S0019-9958(63)90290-0
URL : http://doi.org/10.1016/s0019-9958(63)90290-0

A. Roscoe, The theory and practice of concurrency, 1997.

R. Segala, Modelling and Verification of Randomized Distributed Real Time Systems, 1995.

R. Segala and N. Lynch, Probabilistic simulations for probabilistic processes, Nordic Journal of Computing, vol.2, issue.2, pp.250-273, 1995.
DOI : 10.1007/bfb0015027
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.6430

A. Sokolova and E. De-vink, Probabilistic Automata: System Types, Parallel Composition and Comparison, Validation of Stochastic Systems: A Guide to Current Research, pp.1-43, 2004.
DOI : 10.1007/978-3-540-24611-4_1

W. Stewart, Introduction to the Numerical Solution of Markov Chains, 1994.

M. Vardi, Automatic verification of probabilistic concurrent finite state programs, 26th Annual Symposium on Foundations of Computer Science (sfcs 1985), pp.327-338, 1985.
DOI : 10.1109/SFCS.1985.12

M. Vardi and P. Wolper, Reasoning about Infinite Computations, Information and Computation, vol.115, issue.1, pp.1-37, 1994.
DOI : 10.1006/inco.1994.1092

L. Zhang, H. Hermanns, K. Namjoshi, T. Yoneda, T. Higashino et al., Deciding Simulations on Probabilistic Automata, Proc. 5th Int. Symp. Automated Technology for Verification and Analysis (ATVA'07), pp.207-222, 2007.
DOI : 10.1007/978-3-540-75596-8_16

L. Zhang and M. Neuhäußer, Model Checking Interactive Markov Chains, Proc. 16th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'10), pp.53-68, 2010.
DOI : 10.1007/978-3-642-12002-2_5

L. Zhang, Z. She, S. Ratschan, H. Hermanns, and E. Hahn, Safety verification for probabilistic hybrid systems, Proc. 22nd Int. Conf. Computer Aided Verification (CAV'10), pp.196-211, 2008.