PV4 ⊧ FACT: Formal verification with confidence intervalscomputes confidence intervals for given properties of timed automata

Probabilistic model checker that can compute confidence intervals for certain properties for which observations of the transitions associated with unknown probabilities are available.

Application domain/field

• Quantitative verification
• Probabilistic model checking
• Model checking

Type of tool

Model checker

Expected input

• Parametric Markov chain (PMC)
• PCTL property
• Range of confidence levels

Format:

• PMC: Extended version of PRISM language
• PCTL property: ?
• Range of confidence intervals:

Expected output

Confidence interval for each confidence level $\alpha$ from the user-specified range

Internals

FACT uses a four-step approach:

1. Parametric quantitative verification is used to obtain an algebraic expressed for the analysed PCTL property (uses PRISM)
2. Simultaneous confidence intervals are calculated for each set of parameters
3. Uses results of step 2 for a convex optimisation problem whose solution represents an $\alpha$ confidence interval for the analysed property
4. Uses a heuristic to seek alternative confidence intervals. This optimisation might reduce the width of property confidence intervals.

Comments

License: GNU General Public LIcense