A Probabilistic Choreography Language for PRISM

Explore a choreographic framework for modeling and analyzing concurrent probabilistic systems using the PRISM model-checker in this 19-minute conference talk. Discover how a newly developed choreography language allows for describing desired interactions within concurrent systems from a global perspective. Learn about the benefits of employing choreographies, including improved system reliability and error detection. Delve into the language's probabilistic semantics and its formal encoding into the PRISM language. Understand how properties of programs written in this choreographic language can be model-checked using PRISM. Examine the implementation of a compiler for the language and see practical applications through examples from PRISM website use cases. Presented by Marco Carbone and Adele Veschetti at the CP 2024 workshop, this talk showcases cutting-edge research in probabilistic system modeling and analysis.