A Probabilistic Choreography Language for PRISM

Marco Carbone; Adele Veschetti

doi:10.1007/978-3-031-62697-5_2

A Probabilistic Choreography Language for PRISM

Marco Carbone
, Adele Veschetti

Darmstadt University of Technology

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

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. Employing choreographies provides a clear and comprehensive view of system interactions, enabling the discernment of process flow and detection of potential errors, thus ensuring accurate execution and enhancing 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.

Original language	English
Title of host publication	LNCS
Number of pages	18
Volume	14676
Publisher	Springer
Publication date	2024
Pages	20-37
ISBN (Print)	978-3-031-62696-8
ISBN (Electronic)	978-3-031-62697-5
DOIs	https://doi.org/10.1007/978-3-031-62697-5_2
Publication status	Published - 2024
Event	International Conference on Coordination Models and Languages - Groningen, Netherlands Duration: 17 Jun 2024 → 21 Jun 2024 Conference number: 26 https://link.springer.com/conference/coordination

Conference

Conference	International Conference on Coordination Models and Languages
Number	26
Country/Territory	Netherlands
City	Groningen
Period	17/06/2024 → 21/06/2024
Internet address	https://link.springer.com/conference/coordination

Keywords

Choreographic programming
Probabilistic concurrent systems
Model checking
PRISM model-checker
Formal encoding and compilation

Access to Document

10.1007/978-3-031-62697-5_2

Cite this

@inproceedings{5eee6e9583f544f780df8f3fe4075c1e,

title = "A Probabilistic Choreography Language for PRISM",

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. Employing choreographies provides a clear and comprehensive view of system interactions, enabling the discernment of process flow and detection of potential errors, thus ensuring accurate execution and enhancing 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.",

keywords = "Choreographic programming, Probabilistic concurrent systems, Model checking, PRISM model-checker, Formal encoding and compilation",

author = "Marco Carbone and Adele Veschetti",

year = "2024",

doi = "10.1007/978-3-031-62697-5\_2",

language = "English",

isbn = "978-3-031-62696-8",

volume = "14676",

pages = "20--37",

booktitle = "LNCS",

publisher = "Springer",

address = "Germany",

note = "International Conference on Coordination Models and Languages, COORDINATION ; Conference date: 17-06-2024 Through 21-06-2024",

url = "https://link.springer.com/conference/coordination",

}

TY - GEN

T1 - A Probabilistic Choreography Language for PRISM

AU - Carbone, Marco

AU - Veschetti, Adele

N1 - Conference code: 26

PY - 2024

Y1 - 2024

N2 - 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. Employing choreographies provides a clear and comprehensive view of system interactions, enabling the discernment of process flow and detection of potential errors, thus ensuring accurate execution and enhancing 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.

AB - 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. Employing choreographies provides a clear and comprehensive view of system interactions, enabling the discernment of process flow and detection of potential errors, thus ensuring accurate execution and enhancing 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.

KW - Choreographic programming

KW - Probabilistic concurrent systems

KW - Model checking

KW - PRISM model-checker

KW - Formal encoding and compilation

U2 - 10.1007/978-3-031-62697-5_2

DO - 10.1007/978-3-031-62697-5_2

M3 - Article in proceedings

SN - 978-3-031-62696-8

VL - 14676

SP - 20

EP - 37

BT - LNCS

PB - Springer

T2 - International Conference on Coordination Models and Languages

Y2 - 17 June 2024 through 21 June 2024

ER -

A Probabilistic Choreography Language for PRISM

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this