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.
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.
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.
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.
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.
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.
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.
J. Kemeny, J. Snell & A. Knapp (1976):
Denumerable Markov Chains,
2nd edition.
Springer.
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.
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.
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.
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.
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).
PRISM Case Studies.
http://www.prismmodelchecker.org/casestudies.
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.
UPPAAL Case Studies.
http://www.it.uu.se/research/group/darts/uppaal/examples.shtml.
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.