PV0 ⊧ SLURF

Application domain/field

• Continuous-time Markov chains (CTMCs)
• Probabilistic systems
• Model checking

Expected input

• CTMC (Continuous-time Markov Chain)
• Parameter probability distribution file that defines the probability distributions of the parameters
• Property definition file that defines the properties that are verified by Storm
• Number of samples
• Confidence level

Format:

• CTMC: model file, in the PRISM language for parametric CTMCs and the Galileo format for parametric fault trees.
• Parameter probability distribution file: Excel or CSV (semi-colon separated) file
• Property definition file: Excel or CSV (semi-colon separated) file
• Others are passed as parameters when executing the python script.

Expected output

Prediction region (as image(s))

Internals

Uses Storm SLURF computes prediction regions. This is useful since there are many cases where you are not sure what the exact transition rates or probabilities are. The prediction regions can depict how the uncertainty in the input influences the output. Intuitively this gives some feeling for the robustness of the output for some uncertain input.