一句话：提出一种概率编排语言，定义概率语义并编码到 PRISM，支持并发概率系统的全局建模与模型检测。
论文针对并发概率系统的建模与分析，提出一种基于 PRISM 的编排框架。编排语言从全局视角描述系统内期望的交互，使流程与潜在错误更易理解，从而提高执行正确性与可靠性。作者为该语言赋予概率语义，并给出到 PRISM 语言的形式化编码，讨论编码正确性，使程序性质可通过 PRISM 模型检测器验证。最后实现编译器，并借助 PRISM 网站中的用例展示其实用性，表明该语言可把全局编排规约编译为可分析的概率模型。
We present a choreographic framework for modelling and analysing concurrent probabilistic systems based on the PRISM model-checker. This is achieved through the development of a choreography language, which is a specification language that allows to describe the desired interactions within a concurrent system from a global viewpoint. Using choreographies gives a clear and complete view of system interactions, making it easier to understand the process flow and identify potential errors, which helps ensure correct execution and improves system reliability. We equip our language with a probabilistic semantics and then define a formal encoding into the PRISM language and discuss its correctness. Properties of programs written in our choreographic language can be model-checked by the PRISM model-checker via their translation into the PRISM language. Finally, we implement a compiler for our language and demonstrate its practical applicability via examples drawn from the use cases featured in the PRISM website.