R. Alur, C. Courcoubetis, and D. Dill, Model-checking in dense real-time. Information and Computation, pp.2-34, 1993.

D. Beauquier, On probabilistic timed automata, Theoretical Computer Science, vol.292, issue.1, pp.65-84, 2003.
DOI : 10.1016/S0304-3975(01)00215-8

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

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, 2010.
DOI : 10.1109/QEST.2010.41

N. Blanc, D. Kroening, and N. Sharygina, Scoot: A Tool for the Analysis of SystemC??Models, Proc. TACAS'08, pp.467-470, 2008.
DOI : 10.1007/978-3-540-78800-3_36

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

E. Clarke, D. Kroening, N. Sharygina, and K. Yorav, Predicate abstraction of ANSI-C programs using SAT. Formal Methods in System Design, pp.105-127, 2004.

A. Condon, The complexity of stochastic games. Information and Computation, pp.203-224, 1992.

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973

URL : https://hal.archives-ouvertes.fr/inria-00528590

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.

C. Daws, M. Kwiatkowska, and G. Norman, Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM, International Journal on Software Tools for Technology Transfer, vol.est, issue.1+2, pp.2-3221, 2004.
DOI : 10.1007/s100090050010

L. De-alfaro and P. Roy, Magnifying-Lens Abstraction for Markov Decision Processes
DOI : 10.1007/978-3-540-73368-3_38

H. Dierks, S. Kupferschmid, and K. Larsen, Automatic Abstraction Refinement for Timed Automata, Proc. 5th International Conference on Formal Modelling and Analysis of Timed Systems (FOR- MATS'07), pp.114-129, 2007.
DOI : 10.1007/978-3-540-75454-1_10

R. Drechsler and D. Grosse, Reachability analysis for formal verification of SystemC, Proceedings Euromicro Symposium on Digital System Design. Architectures, Methods and Tools, p.337, 2002.
DOI : 10.1109/DSD.2002.1115387

S. Graf and H. Saidi, Construction of abstract state graphs with PVS, Proc. 9th International Conference on Computer Aided Verification (CAV'97, pp.72-83, 1997.
DOI : 10.1007/3-540-63166-6_10

D. Grosse, U. Kühne, and R. Drechsler, HW/SW co-verification of embedded systems using bounded model checking, Proc. 16th ACM Great Lakes Symposium on VLSI, pp.43-48, 2006.

A. Hartmanns and H. Hermanns, A Modest Approach to Checking Probabilistic Timed Automata, 2009 Sixth International Conference on the Quantitative Evaluation of Systems, pp.187-196, 2009.
DOI : 10.1109/QEST.2009.41

T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, Symbolic model checking for real-time systems, [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, pp.193-244, 1994.
DOI : 10.1109/LICS.1992.185551

P. Herber, J. Fellmuth, and S. Glesner, Model checking SystemC designs using timed automata, Proceedings of the 6th IEEE/ACM/IFIP international conference on Hardware/Software codesign and system synthesis, CODES/ISSS '08, pp.131-136, 2008.
DOI : 10.1145/1450135.1450166

A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker, PRISM: A Tool for Automatic Verification of Probabilistic Systems, Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06), pp.441-444, 2006.
DOI : 10.1007/11691372_29

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

D. Karlsson, P. Eles, and Z. Peng, Formal Verification of SystemC Designs Using a Petri-Net Based Representation, Proceedings of the Design Automation & Test in Europe Conference, pp.1228-1233, 2006.
DOI : 10.1109/DATE.2006.244076

J. Katoen, E. 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, 2009.

M. Kattenbelt, M. Kwiatkowska, G. Norman, and D. Parker, Abstraction Refinement for Probabilistic Software, Proc
DOI : 10.1007/978-3-540-93900-9_17

M. Kattenbelt, M. Kwiatkowska, G. Norman, and D. Parker, A game-based abstraction-refinement 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

S. Kemper and A. Platzer, SAT-based Abstraction Refinement for Real-time Systems, Proc. FACS 2006, pp.107-122, 2007.
DOI : 10.1016/j.entcs.2006.09.034

D. Kroening and N. Sharygina, Formal verification of SystemC by automatic hardware/software partitioning, Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2005. MEMOCODE '05., pp.101-110, 2005.
DOI : 10.1109/MEMCOD.2005.1487900

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

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, A Framework for Verification of Software with Time and Probabilities, Proc. 8th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'10), 2010.
DOI : 10.1007/978-3-642-15297-9_4

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

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, 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

S. Lahiri, T. Ball, and B. Cook, Predicate abstraction via symbolic decision procedures, Proc. 17th International Conference on Computer Aided Verification (CAV'05), pp.24-38, 2005.
DOI : 10.1007/11513988_5

URL : http://arxiv.org/abs/cs/0612003

K. Larsen, P. Pettersson, and W. Yi, Uppaal in a nutshell, International Journal on Software Tools for Technology Transfer, vol.1, issue.1-2, pp.134-152, 1997.
DOI : 10.1007/s100090050010

M. Moy, F. Maraninchi, and L. Maillet-contoz, Pinapa, Proceedings of the 5th ACM international conference on Embedded software , EMSOFT '05, pp.317-324, 2005.
DOI : 10.1145/1086228.1086286

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

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

L. Shapley, Stochastic games, Proc. National Academy of Science, pp.1095-1100, 1953.

M. Sorea, Lazy Approximation for Dense Real-Time Systems, Proc. Joint International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS) and Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT), pp.363-378, 2004.
DOI : 10.1007/978-3-540-30206-3_25

C. Traulsen, J. Cornet, M. Moy, and F. Maraninchi, A SystemC/TLM Semantics in Promela and Its Possible Applications, Proc. 14th Int. SPIN Workshop on Model Checking of Software (SPIN'07), pp.204-222, 2007.
DOI : 10.1007/978-3-540-73370-6_14

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

S. Tripakis, The formal analysis of timed systems in practice, 1998.
URL : https://hal.archives-ouvertes.fr/tel-00004907

M. Vardi, Formal techniques for SystemC verification, Proceedings of the 44th annual conference on Design automation, DAC '07, pp.188-192, 2007.
DOI : 10.1145/1278480.1278527

B. Wachter and L. Zhang, Best Probabilistic Transformers, Proc. 11th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'10), pp.362-379, 2010.
DOI : 10.1007/978-3-642-11319-2_26

A. Zbrzezny and P. Lrola, SAT-based reachability checking for timed automata with discrete data, Fundamenta Informaticae, vol.79, issue.3-4, pp.579-593, 2008.