# 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.