A Probabilistic Choreography Language for PRISM

on YouTube ↗19m

" summary

A choreographic specification language gives global descriptions of concurrent probabilistic interactions, defines a probabilistic semantics, and provides a formal, correctness-proved translation into the PRISM model language so properties can be model-checked there. The authors implement a compiler that emits PRISM code and validate it on examples from the PRISM website, showing the approach encodes real workflows and lets PRISM verify behavioral and quantitative properties automatically.

AI-written summary · about

" chapters (12)

1. 0:00Introduction
2. 0:22Function as a service context
3. 4:12Serverless locality challenges
4. 5:41Workflow composition in FaaS
5. 7:50FCAL choreography language
6. 8:32Distributed neural network use case
7. 10:19FCAL code structure
8. 11:00FCAL behavior and data flow
9. 13:29Locality constraints extraction
10. 15:15Scheduling preferences from FCAL
11. 16:42FCAL future directions
12. 17:26Q&A