@article(BT91,
 author       = "D. P. Bertsekas and J. N. Tsitsiklis",
 year         = "1991",
 title        = "An Analysis of Stochastic Shortest Path Problems",
 journal      = "Mathematics of Operations Research",
 volume       = "16",
 number       = "3",
 pages        = "580--595",
 doi          = "10.1287/moor.16.3.580",
)
@inproceedings(CHK08,
 author       = "T. {Chen} and T. {Han} and J. P. {Katoen}",
 year         = "2008",
 title        = "Time-Abstracting Bisimulation for Probabilistic Timed Automata",
 booktitle    = "TASE'08",
 publisher    = "IEEE Comp. Soc.",
 pages        = "177--184",
 doi          = "10.1109/TASE.2008.29",
)
@misc(WSLA,
 author       = "A. Dan and R. Franck and A. Keller and R. King and H. Ludwig",
 year         = "2002",
 title        = "{Web Service Level Agreement (WSLA)} Language Specification",
 url          = "http://www.research.ibm.com/wsla/documents.html",
)
@incollection(GGMT08,
 author       = "S. Gallotti and C. Ghezzi and R. Mirandola and G. Tamburrelli",
 year         = "2008",
 title        = "Quality Prediction of Service Compositions through Probabilistic Model Checking",
 booktitle    = "QoSA'08",
 series       = "LNCS 5281",
 publisher    = "Springer",
 pages        = "119--134",
 doi          = "10.1007/978-3-540-87879-7\_8",
)
@inproceedings(JL91,
 author       = "B. Jonsson and K. G. Larsen",
 year         = "1991",
 title        = "Specification and Refinement of Probabilistic Processes",
 booktitle    = "LICS'91",
 publisher    = "IEEE Comp. Soc.",
 pages        = "266--277",
 doi          = "10.1109/LICS.1991.151651",
)
@article(JSL08,
 author       = "M. Jurdzinski and J. Sproston and F. Laroussinie",
 year         = "2008",
 title        = "Model Checking Probabilistic Timed Automata with One or Two Clocks",
 journal      = "Log. Meth. in Comp. Sci.",
 volume       = "4",
 number       = "3",
 doi          = "10.2168/LMCS-4(3:12)2008",
)
@article(JHF09,
 author       = "I. Jureta and C. Herssens and S. Faulkner",
 year         = "2009",
 title        = "A comprehensive quality model for service-oriented systems",
 journal      = "Software Quality Journal",
 volume       = "17",
 pages        = "65--98",
 doi          = "10.1007/s11219-008-9059-2",
)
@article(KL03,
 author       = "A. Keller and H. Ludwig",
 year         = "2003",
 title        = "The {WSLA} Framework: Specifying and Monitoring Service Level Agreements for Web Services",
 journal      = "J. Netw. Syst. Manage.",
 volume       = "11",
 pages        = "2003",
 doi          = "10.1023/A:1022445108617",
)
@book(KSK76,
 author       = "J. Kemeny and J. Snell and A. Knapp",
 year         = "1976",
 title        = "Denumerable {M}arkov Chains",
 edition      = "2nd",
 publisher    = "Springer",
)
@inproceedings(KNP11,
 author       = "M. Kwiatkowska and G. Norman and D. Parker",
 year         = "2011",
 title        = "{PRISM} 4.0: Verification of Probabilistic Real-time Systems",
 booktitle    = "CAV'11",
 series       = "LNCS 6806",
 publisher    = "Springer",
 pages        = "585--591",
 doi          = "10.1007/978-3-642-22110-1\_47",
)
@article(KNPS06,
 author       = "M. Kwiatkowska and G. Norman and D. Parker and J. Sproston",
 year         = "2006",
 title        = "Performance Analysis of Probabilistic Timed Automata using Digital Clocks",
 journal      = "Form. Methods Syst. Des.",
 volume       = "29",
 pages        = "33--78",
 doi          = "10.1007/s10703-006-0005-2",
)
@article(KGSS02,
 author       = "M. Kwiatkowska and G. Norman and R. Segala and J. Sproston",
 year         = "2002",
 title        = "Automatic verification of real-time systems with discrete probability distributions",
 journal      = "Theor. Comput. Sci.",
 volume       = "282",
 pages        = "101--150",
 doi          = "10.1016/S0304-3975(01)00046-9",
)
@article(KNSW04,
 author       = "M. Kwiatkowska and G. Norman and J. Sproston and F. Wang",
 year         = "2007",
 title        = "Symbolic model checking for probabilistic timed automata",
 journal      = "Inf. Comput.",
 volume       = "205",
 pages        = "1027--1077",
 doi          = "10.1016/j.ic.2007.01.004",
)
@article(MSKA11,
 author       = "Y.-J. Moon and A. Silva and C. Krause and F. Arbab",
 year         = "2011",
 title        = "A Compositional Model to Reason about end-to-end {QoS} in Stochastic {Reo} Connectors",
 journal      = "Science of Computer Programming (to appear)",
)
@misc(PRISMCaseStudies,
 title        = "{PRISM Case Studies}",
 howpublished = "\url {http://www.prismmodelchecker.org/casestudies}",
)
@incollection(SVA06,
 author       = "K. Sen and M. Viswanathan and G. Agha",
 year         = "2006",
 title        = "Model-Checking {Markov} Chains in the Presence of Uncertainties",
 booktitle    = "TACAS'06",
 series       = "LNCS 3920",
 publisher    = "Springer",
 pages        = "394--410",
 doi          = "10.1007/11691372\_26",
)
@misc(UPPAALCaseStudies,
 title        = "{UPPAAL Case Studies}",
 howpublished = "\url {http://www.it.uu.se/research/group/darts/uppaal/examples.shtml}",
)
@inproceedings(IPTA,
 author       = "J. Zhang and J. Zhao and Z. Huang and Z. Cao",
 year         = "2009",
 title        = "Model Checking Interval Probabilistic Timed Automata",
 booktitle    = "ICISE'09",
 publisher    = "IEEE Comp. Soc.",
 pages        = "4936--4940",
 doi          = "10.1109/ICISE.2009.749",
)