A Probabilistic Choreography Language for PRISM
This work addresses the challenge of ensuring correct execution and reliability in concurrent probabilistic systems for researchers and practitioners in formal methods and model-checking, though it is incremental as it builds on existing PRISM frameworks.
The authors tackled the problem of modeling and analyzing concurrent probabilistic systems by developing a choreography language for the PRISM model-checker, enabling easier understanding and verification of system interactions through a formal encoding and compiler implementation.
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.