PV4 ⊧ FACT: Formal verification with confidence intervalscomputes confidence intervals for given properties of timed automataProbabilistic model checker that can compute confidence intervals for certain properties for which observations of the transitions associated with unknown probabilities are available.
- Quantitative verification
- Probabilistic model checking
- Model checking
Type of toolModel checker
- Parametric Markov chain (PMC)
- PCTL property
- Range of confidence levels
- PMC: Extended version of PRISM language
- PCTL property: ?
- Range of confidence intervals:
Expected outputConfidence interval for each confidence level from the user-specified range
InternalsFACT uses a four-step approach:
- Parametric quantitative verification is used to obtain an algebraic expressed for the analysed PCTL property (uses PRISM)
- Simultaneous confidence intervals are calculated for each set of parameters
- Uses results of step 2 for a convex optimisation problem whose solution represents an confidence interval for the analysed property
- Uses a heuristic to seek alternative confidence intervals. This optimisation might reduce the width of property confidence intervals.