Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Probabilistic Choreography Language for PRISM

Marco Carbone, Adele Veschetti

TL;DR

The paper addresses the challenge of modeling and verifying concurrent probabilistic systems by introducing a probabilistic choreographic language that expresses global interaction patterns. It defines formal syntax and operational semantics, develops a minimal PRISM fragment for code generation, and proves correctness of a translation (projection) from choreographies to PRISM models. A practical Java-based implementation and compiler demonstrate the end-to-end flow from choreography to PRISM code, enabling model checking of global specifications with standard PRISM analyses. Benchmarking across diverse protocols shows the approach yields concise, readable models that preserve the behavior of reference PRISM specifications, with insights into applicability and limitations. The work offers a usable, correct-by-construction path from high-level probabilistic choreography to provable, analyzable PRISM models, facilitating reliable design of distributed systems.

Abstract

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.

A Probabilistic Choreography Language for PRISM

TL;DR

The paper addresses the challenge of modeling and verifying concurrent probabilistic systems by introducing a probabilistic choreographic language that expresses global interaction patterns. It defines formal syntax and operational semantics, develops a minimal PRISM fragment for code generation, and proves correctness of a translation (projection) from choreographies to PRISM models. A practical Java-based implementation and compiler demonstrate the end-to-end flow from choreography to PRISM code, enabling model checking of global specifications with standard PRISM analyses. Benchmarking across diverse protocols shows the approach yields concise, readable models that preserve the behavior of reference PRISM specifications, with insights into applicability and limitations. The work offers a usable, correct-by-construction path from high-level probabilistic choreography to provable, analyzable PRISM models, facilitating reliable design of distributed systems.

Abstract

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.

Paper Structure

This paper contains 23 sections, 1 theorem, 25 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Contributions and Overview.
  3. Changes with respect to the conference version.
  4. A Motivating Example
  5. Choreography Language
  6. Syntax
  7. Semantics.
  8. Other language constructs
  9. The PRISM Language
  10. Syntax.
  11. Semantics.
  12. Projection
  13. Mapping Choreographies to PRISM
  14. Correctness.
  15. Implementation
  16. ...and 8 more sections

Key Result

Theorem 1

Given a choreography $C$ such that $\mathsf{sConn}(C)$, we have that $(S,C) \ \longrightarrow_{\lambda}\ (S', C')$ if and only if $|\!|_{\mathtt{q}\in C}\ \mathsf{proj} (\mathtt{q}, C,\iota)\vdash S_{+} \ \longrightarrow_{\lambda}\ S_{+}'$.

Figures (7)

  • Figure 1: Semantics for PRISM networks
  • Figure 2: Probability that clients received all the blocks before $T$, with $0\leq T \leq 1.5$
  • Figure 3: Probability that a block is created within $T$ time units, $0\leq T\leq 1000$
  • Figure 4: Probability that a block is created within $T$ time units, $0\leq T\leq 200$
  • Figure 5: The probability of electing a leader within $L$ rounds, with $1 \leq L \leq 10$
  • ...and 2 more figures

Theorems & Definitions (13)

  • Definition 1
  • Example 1
  • Example 2
  • Example 3
  • Example 4
  • Definition 2: Annotated Choreography
  • Definition 3: Projection, CTMC
  • Example 5
  • Definition 4: Projection, DTMC
  • Definition 5: Head Modules
  • ...and 3 more