A. Aziz, K. Sanwal, V. Singhal, and R. Brayton, Towards Performance Prediction of Verifying Continuous Time Markov Chains, LNCS, vol.1102, pp.269-276, 1996.
DOI : 10.1007/3-540-61474-5_75
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.3391

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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.68.2348

C. Baier, H. Hermanns, J. 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. Katoen, Principles of Model Checking, 2008.

A. Bianco and . Luca-de-alfaro, Model checking of probabilistic and nondeterministic systems, FSTTCS LNCS, vol.1026, pp.499-513, 1995.
DOI : 10.1007/3-540-60692-0_70
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.7155

E. Böde, M. Herbstritt, H. Hermanns, S. Johr, T. Peikenkamp et al., Compositional Dependability Evaluation for STATEMATE, IEEE Transactions on Software Engineering, vol.35, issue.2, pp.274-292, 2009.
DOI : 10.1109/TSE.2008.102

M. Bravetti, H. Hermanns, and J. Katoen, YMCA, Electronic Notes in Theoretical Computer Science, vol.162, pp.107-112, 2006.
DOI : 10.1016/j.entcs.2005.12.108

T. Brázdil and H. Hermanns-kr?ál, K?etínsk´K?etínsk´y and Vojt?chVojt?ch?Vojt?ch?ehák: Verification of Open Interactive Markov Chains, FSTTCS, pp.474-485, 2012.

L. Cloth and R. Boudewijn, Haverkort: Model Checking for Survivability. QEST, pp.145-154, 2005.
DOI : 10.1109/qest.2005.21
URL : http://purl.utwente.nl/publications/55783

N. Coste, H. Hermanns, and E. Lantreibecq, Wendelin Serwe: Towards Performance Prediction of Compositional Models in Industrial GALS Designs, LNCS, vol.5643, pp.204-218, 2009.

N. Coste, H. Garavel, H. Hermanns, R. Hersemeule, Y. Thonnart et al., Quantitative evaluation in embedded system design, Proceedings of the conference on Design, automation and test in Europe, DATE '08, pp.88-89, 2008.
DOI : 10.1145/1403375.1403399
URL : https://hal.archives-ouvertes.fr/inria-00199914

C. Eisentraut and H. Hermanns, Lijun Zhang: On Probabilistic Automata in Continuous Time, LICS, pp.342-351, 2010.
DOI : 10.1109/lics.2010.41
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.484.1720

M. Esteve, J. Katoen, B. Viet-yen-nguyen, Y. Postma, and . Yushtein, Formal correctness, safety, dependability, and performance analysis of a satellite, 2012 34th International Conference on Software Engineering (ICSE), pp.1022-1031, 2012.
DOI : 10.1109/ICSE.2012.6227118

H. Garavel, F. Lang, and R. Mateescu, Wendelin Serwe: CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes, TACAS LNCS, vol.6605, pp.372-387, 2011.

D. Guck, Quantitative Analysis of Markov Automata Master Thesis, 2012.

D. Guck, T. Han, J. Katoen, and M. R. Neuhäusser, Quantitative Timed Analysis of Interactive Markov Chains, NASA Formal Methods, pp.8-23, 2012.
DOI : 10.1007/978-3-642-28891-3_4

H. Hatefi and H. Hermanns, Model Checking Algorithms for Markov Automata, ECEASST, p.53, 2012.

H. Hermanns, U. Herzog, and J. Katoen, Process algebra for performance evaluation, Theoretical Computer Science, vol.274, issue.1-2, pp.43-87, 2002.
DOI : 10.1016/S0304-3975(00)00305-4
URL : http://doi.org/10.1016/s0304-3975(00)00305-4

H. Hermanns and J. Katoen, Automated compositional Markov chain generation for a plain-old telephone system, Science of Computer Programming, vol.36, issue.1, pp.97-127, 2000.
DOI : 10.1016/S0167-6423(99)00019-2
URL : http://doi.org/10.1016/s0167-6423(99)00019-2

V. Hermenegildamacì-a, F. Valero, M. C. Cuartero, and . Ruiz, sPBC: A Markovian Extension of Petri Box Calculus with Immediate Multiactions, Fundamenta Informaticae, vol.87, pp.3-4367, 2008.

R. Martin, Neuhäusser: Model Checking Nondeterministic and Randomly Timed Systems, 2010.

R. Boudewijn, M. Haverkort, A. Kuntz, S. Remke, M. Roolvink et al., Evaluating repair strategies for a water-treatment facility using Arcade, pp.419-424, 2010.

R. Pulungan, Reduction of Acyclic Phase-Type Representations, 2009.

L. Zhang and R. Martin, Neuhäusser: Model Checking Interactive Markov Chains, TACAS LNCS, vol.6015, pp.53-68, 2010.

L. Zhang, D. N. Jansen, and F. Nielson, Holger Hermanns: Automata- Based CSL Model Checking, ICALP, pp.271-282, 2011.
DOI : 10.1007/978-3-642-22012-8_21