H. Aljazzar and S. Leue, Directed Explicit State-Space Search in the Generation of Counterexamples for Stochastic Model Checking, IEEE Transactions on Software Engineering, vol.36, issue.1, pp.37-60, 2010.
DOI : 10.1109/TSE.2009.57

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. 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), pp.129-148, 2008.
DOI : 10.1007/978-3-540-24611-4_1

D. Angluin, J. Aspnes, and D. Eisenstat, A simple population protocol for fast robust approximate majority, Distributed Computing, pp.87-102, 2008.

C. Baier, E. Clarke, V. Hartonas-garmhausen, M. Kwiatkowska, and M. Ryan, Symbolic model checking for probabilistic processes, Proc. 24th International Colloquium on Automata, Languages and Programming (ICALP'97 volume 1256 of LNCS, pp.430-440, 1997.
DOI : 10.1007/3-540-63165-8_199

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., pp.230-239, 2004.
DOI : 10.1109/QEST.2004.1348037

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

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

C. Baier and J. 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

J. Berendsen, D. Jansen, and J. Katoen, Probably on time and within budget ? on reachability in priced probabilistic timed automata, Proc. 3rd International Conference on Quantitative Evaluation of Systems (QEST'06), pp.311-322, 2006.

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

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

P. Cern´ycern´y, K. Chatterjee, T. Henzinger, A. Radhakrishna, and R. Singh, Quantitative synthesis for concurrent programs, Proc. 23rd International Conference on Computer Aided Verification (CAV'11), pp.243-259, 2011.

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

K. Chatterjee, T. Henzinger, B. Jobstmann, and R. Singh, Measuring and synthesizing systems in probabilistic environments, Proc. 22nd International Conference on Computer Aided Verification (CAV'10), 2010.

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

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

E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-guided abstraction refinement, Proc. 12th Int. Conf. Computer Aided Verification (CAV'00), volume 1855 of Lecture Notes in Computer Science, pp.154-169, 2000.
DOI : 10.1109/time.2003.1214874
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.19.407

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

P. D. Argenio, B. Jeannet, H. Jensen, and K. Larsen, Reachability analysis of probabilistic systems by successive refinements, Proc. 1st Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modelling and Verification (PAPM/PROBMIV'01), volume 2165 of LNCS, pp.39-56, 2001.

P. D. Argenio and P. Niebert, Partial order reduction on concurrent probabilistic programs, Proc. 1st International Conference on Quantitative Evaluation of Systems

L. De-alfaro, M. Kwiatkowska, G. Norman, D. Parker, and R. Segala, Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation, Proc. 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00), volume 1785 of LNCS, pp.395-410, 2000.
DOI : 10.1007/3-540-46419-0_27

L. De-alfaro and P. Roy, Magnifying-Lens Abstraction for Markov Decision Processes, Proc. 19th International Conference on Computer Aided Verification (CAV'07), pp.325-338, 2007.
DOI : 10.1007/978-3-540-73368-3_38

A. Donaldson and A. Miller, Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives, Proc. 4th Int. Symp. Automated Technology for Verification and Analysis (ATVA'06), pp.9-23, 2006.
DOI : 10.1007/11901914_4

J. Esparza and A. Gaiser, Probabilistic Abstractions with Arbitrary Domains, Proc. 18th International Symposium on Static Analysis (SAS'11), pp.334-350, 2011.
DOI : 10.1007/978-3-642-11319-2_26

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

E. M. Hahn, H. Hermanns, B. Wachter, and L. Zhang, PASS: Abstraction Refinement for Infinite Probabilistic Models, Proc. 16th International Conference on 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. M. Hahn, H. Hermanns, and L. Zhang, Probabilistic reachability for parametric Markov models, Proc. 16th International SPIN Workshop, pp.88-106, 2009.
DOI : 10.1007/s10009-010-0146-x
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.184.3136

E. M. Hahn, G. Norman, D. Parker, B. Wachter, and L. Zhang, Game-based Abstraction and Controller Synthesis for Probabilistic Hybrid Systems, 2011 Eighth International Conference on Quantitative Evaluation of SysTems, pp.69-78, 2011.
DOI : 10.1109/QEST.2011.17
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.678.579

T. Han, J. Katoen, and B. Damman, Counterexample generation in probabilistic model checking, IEEE Transactions on Software Engineering, vol.35, issue.2, pp.241-257, 2009.

T. Han, J. 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

S. Hart, M. Sharir, and A. Pnueli, Termination of Probabilistic Concurrent Program, ACM Transactions on Programming Languages and Systems, vol.5, issue.3, pp.356-380, 1983.
DOI : 10.1145/2166.357214

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

T. Henzinger, M. Mateescu, L. Mikeev, and V. Wolf, Hybrid numerical solution of the chemical master equation, Proceedings of the 8th International Conference on Computational Methods in Systems Biology, CMSB '10, pp.55-65, 2010.
DOI : 10.1145/1839764.1839772

T. Hérault, R. Lassaigne, F. Magniette, and S. Peyronnet, Approximate Probabilistic Model Checking, Proc. 5th International Conference on Verification, Model Checking and Abstract Interpretation, 2004.
DOI : 10.1007/978-3-540-24622-0_8

H. Hermanns, J. Katoen, J. Meyer-kayser, and M. Siegle, A Markov Chain Model Checker, Proc. 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00), volume 1785 of LNCS, pp.347-362, 2000.
DOI : 10.1007/3-540-46419-0_24

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

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

J. Katoen, T. Kemna, I. Zapreev, and D. Jansen, Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking, Proc. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'07), pp.87-101, 2007.
DOI : 10.1007/978-3-540-71209-1_9

M. Kattenbelt, M. Kwiatkowska, G. Norman, and D. Parker, Game-Based Probabilistic Predicate Abstraction in PRISM, Proc. 6th Workshop on Quantitative Aspects of Programming Languages, 2008.
DOI : 10.1016/j.entcs.2008.11.016

M. Kattenbelt, M. Kwiatkowska, G. Norman, and D. Parker, Abstraction Refinement for Probabilistic Software, Proc. 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'09), pp.182-197, 2009.
DOI : 10.1007/978-3-540-93900-9_17

M. Kattenbelt, M. Kwiatkowska, G. Norman, and D. Parker, A game-based abstractionrefinement framework for Markov decision processes. Formal Methods in System Design, pp.246-280, 2010.

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, Probabilistic symbolic model checking with PRISM: a hybrid approach, International Journal on Software Tools for Technology Transfer, vol.24, issue.2, pp.128-142, 2004.
DOI : 10.1007/s10009-004-0140-2

M. Kwiatkowska, G. Norman, and D. Parker, Probabilistic model checking in practice, ACM SIGMETRICS Performance Evaluation Review, vol.32, issue.4, pp.16-21, 2005.
DOI : 10.1145/1059816.1059820

M. Kwiatkowska, G. Norman, and D. Parker, Game-based abstraction for Markov decision processes, Proc. 3rd International Conference on Quantitative Evaluation of Systems (QEST'06), pp.157-166, 2006.

M. Kwiatkowska, G. Norman, and D. Parker, Symmetry Reduction for Probabilistic Model Checking, Proc. 18th International Conference on 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), 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 International Conference on 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, 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, D. Parker, and H. Qu, Assume-Guarantee Verification for Probabilistic Systems, Proc. 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'10), pp.23-37, 2010.
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, Performance analysis of probabilistic timed automata using digital clocks, Formal Methods in System Design, vol.29, issue.1, pp.33-78, 2006.
DOI : 10.1007/s10703-006-0005-2

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

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

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

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

R. Segala and N. Lynch, Probabilistic simulations for probabilistic processes, Proc. 5th International Conference on Concurrency Theory (CONCUR'94), pp.481-496, 1994.
DOI : 10.1007/bfb0015027
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.6430

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

V. Wolf, R. Goel, M. Mateescu, and T. Henzinger, Solving the chemical master equation using sliding windows, BMC Systems Biology, vol.4, issue.1, 2010.
DOI : 10.1186/1752-0509-4-42

H. Younes and R. Simmons, Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling, Proc. 14th International Conference on Computer Aided Verification, pp.223-235, 2002.
DOI : 10.1007/3-540-45657-0_17