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

Type of tool

Model checker

Expected input


Expected output

Confidence interval for each confidence level α from the user-specified range


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


License: GNU General Public LIcense
Model checking Probabilistic


Project page: http://www-users.cs.york.ac.uk/~cap/FACT

Related papers

FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals (TACAS '16)

Last publication date

9 April 2016

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.