Paper: "Verifying Team Formation Protocols in PRISM" by Taolue Chen, Marta Kwiatkowska, David Parker and Aistis Simaitis.
Included below are models and properties used to generate experimental results in the paper. Models and properties are in standard PRISM format and (where feasible) can be analysed with the default version of PRISM. Stochastic game properties currently require the "prism-games" extension of PRISM (which will be made publicly available in due course) and are provided for information only.