DiVA: http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-315290
PDF: Formally Verifying Decompositions of Stochastic Specifications (With Proofs).pdf