A Probabilistic Choreography Language for PRISM
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866908880510910464 |
|---|---|
| author | Carbone, Marco Veschetti, Adele |
| author_facet | Carbone, Marco Veschetti, Adele |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_08530 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Probabilistic Choreography Language for PRISM Carbone, Marco Veschetti, Adele Logic in Computer Science Programming Languages 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. |
| title | A Probabilistic Choreography Language for PRISM |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2503.08530 |