Paper:
"Pareto Curves for Probabilistic Model Checking"
by Vojtěch Forejt, Marta Kwiatkowska and David Parker.
Included below are all models and properties used to generate experimental results in the paper. Models are in standard PRISM format and can be analysed with the default version of PRISM. Properties currently require the "prism-multi" extension of PRISM (which will be made publicly available in due course) and are provided for information only.
Compositional verification examples (from [KNPQ10])K is the number of probe messages sent by the protocol.
K is the number of probe messages sent by the protocol, T is the time bound encoded into the assumption.
N is the number of agents (sensors) involved in team formation.
K measures the granularity of the timer, i.e. the number of ticks per time unit.
k is the time-bounded used in the property.