1. D. P. Bertsekas & J. N. Tsitsiklis (1991): An Analysis of Stochastic Shortest Path Problems. Mathematics of Operations Research 16(3), pp. 580–595, doi:10.1287/moor.16.3.580.
  2. T. Chen, T. Han & J. P. Katoen (2008): Time-Abstracting Bisimulation for Probabilistic Timed Automata. In: TASE'08. IEEE Comp. Soc., pp. 177–184, doi:10.1109/TASE.2008.29.
  3. A. Dan, R. Franck, A. Keller, R. King & H. Ludwig (2002): Web Service Level Agreement (WSLA) Language Specification. Available at
  4. S. Gallotti, C. Ghezzi, R. Mirandola & G. Tamburrelli (2008): Quality Prediction of Service Compositions through Probabilistic Model Checking. In: QoSA'08, LNCS 5281. Springer, pp. 119–134, doi:10.1007/978-3-540-87879-7_8.
  5. B. Jonsson & K. G. Larsen (1991): Specification and Refinement of Probabilistic Processes. In: LICS'91. IEEE Comp. Soc., pp. 266–277, doi:10.1109/LICS.1991.151651.
  6. M. Jurdzinski, J. Sproston & F. Laroussinie (2008): Model Checking Probabilistic Timed Automata with One or Two Clocks. Log. Meth. in Comp. Sci. 4(3), doi:10.2168/LMCS-4(3:12)2008.
  7. I. Jureta, C. Herssens & S. Faulkner (2009): A comprehensive quality model for service-oriented systems. Software Quality Journal 17, pp. 65–98, doi:10.1007/s11219-008-9059-2.
  8. A. Keller & H. Ludwig (2003): The WSLA Framework: Specifying and Monitoring Service Level Agreements for Web Services. J. Netw. Syst. Manage. 11, pp. 2003, doi:10.1023/A:1022445108617.
  9. J. Kemeny, J. Snell & A. Knapp (1976): Denumerable Markov Chains, 2nd edition. Springer.
  10. M. Kwiatkowska, G. Norman & D. Parker (2011): PRISM 4.0: Verification of Probabilistic Real-time Systems. In: CAV'11, LNCS 6806. Springer, pp. 585–591, doi:10.1007/978-3-642-22110-1_47.
  11. M. Kwiatkowska, G. Norman, D. Parker & J. Sproston (2006): Performance Analysis of Probabilistic Timed Automata using Digital Clocks. Form. Methods Syst. Des. 29, pp. 33–78, doi:10.1007/s10703-006-0005-2.
  12. M. Kwiatkowska, G. Norman, R. Segala & J. Sproston (2002): Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci. 282, pp. 101–150, doi:10.1016/S0304-3975(01)00046-9.
  13. M. Kwiatkowska, G. Norman, J. Sproston & F. Wang (2007): Symbolic model checking for probabilistic timed automata. Inf. Comput. 205, pp. 1027–1077, doi:10.1016/j.ic.2007.01.004.
  14. Y.-J. Moon, A. Silva, C. Krause & F. Arbab (2011): A Compositional Model to Reason about end-to-end QoS in Stochastic Reo Connectors. Science of Computer Programming (to appear).
  15. PRISM Case Studies.
  16. K. Sen, M. Viswanathan & G. Agha (2006): Model-Checking Markov Chains in the Presence of Uncertainties. In: TACAS'06, LNCS 3920. Springer, pp. 394–410, doi:10.1007/11691372_26.
  17. UPPAAL Case Studies.
  18. J. Zhang, J. Zhao, Z. Huang & Z. Cao (2009): Model Checking Interval Probabilistic Timed Automata. In: ICISE'09. IEEE Comp. Soc., pp. 4936–4940, doi:10.1109/ICISE.2009.749.

Comments and questions to:
For website issues: