Encodings are the main way to compare process calculi. By applying quality criteria to encodings we analyse their quality and rule out trivial or meaningless encodings. Thereby, operational correspondence is one of the most common and most important quality criteria. It ensures that processes and their translations have the same abstract behaviour. We analyse probabilistic versions of operational correspondence to enable such a verification for probabilistic systems. Concretely, we present three versions of probabilistic operational correspondence: weak, middle, and strong. We show the relevance of the weaker version using an encoding from a sublanguage of probabilistic CCS into the probabilistic pi-calculus. Moreover, we map this version of probabilistic operational correspondence onto a probabilistic behavioural relation that directly relates source and target terms. Then we can analyse the quality of the criterion by analysing the relation it induces between a source term and its translation. For the second version of probabilistic operational correspondence we proceed in the opposite direction. We start with a standard simulation relation for probabilistic systems and map it onto a probabilistic operational correspondence criterion. This technical report contains the proofs to the lemmata and theorems of [8] as well as some additional material.

翻译：编码是比较进程演算的主要方式。通过将质量准则应用于编码，我们分析其质量并排除琐碎或无意义的编码。其中，操作对应性是最常见且最重要的质量准则之一，它确保进程及其翻译具有相同的抽象行为。我们分析了概率操作对应性的多种版本，以实现对概率系统的此类验证。具体而言，我们提出了三种概率操作对应性版本：弱对应性、中等对应性和强对应性。通过将概率CCS的子语言编码到概率π演算中，我们展示了弱对应性版本的相关性。此外，我们将该版本的概率操作对应性映射到一种直接关联源项和目标项的概率行为关系上，从而通过分析该关系在源项与其翻译之间诱导的关联来评估准则的质量。针对第二版本的概率操作对应性，我们采用反向路径：从概率系统的标准模拟关系出发，将其映射成概率操作对应性准则。本技术报告包含文献[8]中引理和定理的证明，以及一些补充材料。