Skip to content

Commit

Permalink
Formatted the description list, added SMC tutorial to verifying.md
Browse files Browse the repository at this point in the history
  • Loading branch information
mikucionisaau committed May 22, 2024
1 parent 1b2c0c5 commit ce1ebad
Showing 1 changed file with 18 additions and 24 deletions.
42 changes: 18 additions & 24 deletions content/gui-reference/verifier/verifying.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,40 +15,34 @@ In case the _Over Approximation_ or the _Under Approximation_ options are select

Parameters for statistical model checking can be changed in the [Options](/gui-reference/menu-bar/options/) menu. Various data plots (if available) can be accessed via popup-menu by right-clicking the statistical property. The y-axis always denotes a probability or its density, while x-axis denotes either the variable values limited by the statistical query or a step (transition) count in the model run.

<dl>
Probability density distribution
: A histogram created from probability distribution where each bucket is normalized by a bucket width. Useful for comparison of various distributions, potentially with different bucket widths.

<dt>Probability density distribution</dt>
Probability distribution
: A histogram created from a frequency histogram where each bucket is normalized by a total number of runs. Useful for assessing a probability of a property being satisfied at a particular moment in time interval.

<dd>A histogram created from probability distribution where each bucket is normalized by a bucket width. Useful for comparison of various distributions, potentially with different bucket widths.</dd>
Cumulative probability distribution
: A histogram created by adding up all frequency histogram buckets up to the current bucket and normalized by a total number of runs.

<dt>Probability distribution</dt>
Confidence Intervals for Probabilities
: The confidence intervals for probabilities are computed using Clopper-Pearson method (also known as "exact") for binomial distribution for a given level of confidence (1-α). The method is conservative in a sense that it guarantees the minimum coverage of the real probability in (1-α) of cases. In the plots, the estimated confidence is valid only for one bucket at a time (the gathered data is reused to compute each individual bucket).

<dd>A histogram created from a frequency histogram where each bucket is normalized by a total number of runs. Useful for assessing a probability of a property being satisfied at a particular moment in time interval.</dd>
Confidence Intervals for Mean
: The confidence intervals for mean estimation are computed using quantiles of Student's t-distribution for a given level of confidence of 1-α. Note that t-distribution approaches the commonly used Normal (Gaussian) distribution when the number of samples is high.

<dt>Cumulative probability distribution</dt>

<dd>A histogram created by adding up all frequency histogram buckets up to the current bucket and normalized by a total number of runs.</dd>

<dt>Confidence Intervals for Probabilities</dt>

<dd>The confidence intervals for probabilities are computed using Clopper-Pearson method (also known as "exact") for binomial distribution for a given level of confidence (1-α). The method is conservative in a sense that it guarantees the minimum coverage of the real probability in (1-α) of cases. In the plots, the estimated confidence is valid only for one bucket at a time (the gathered data is reused to compute each individual bucket).</dd>

<dt>Confidence Intervals for Mean</dt>

<dd>The confidence intervals for mean estimation are computed using quantiles of Student's t-distribution for a given level of confidence of 1-α. Note that t-distribution approaches the commonly used Normal (Gaussian) distribution when the number of samples is high.</dd>

<dt>Frequency histogram</dt>

<dd>The frequency histogram is created by calculating the number of runs satisfying the property at a particular moment in time interval. Useful for calculating the number of runs.</dd>

</dl>
Frequency histogram
: The frequency histogram is created by calculating the number of runs satisfying the property at a particular moment in time interval. Useful for calculating the number of runs.

Any plot can be customized from a popup menu by right-clicking on the plot.

Further, the plot labels and titles can be edited and several data sets can be superimposed in one figure by using Plot Composer, accessible from the [Tools](/gui-reference/menu-bar/tools/) menu. It is possible to create several composite plots at a time by invoking Plot Composer multiple times.

See also:

> _UPPAAL SMC tutorial_, **Alexandre David**, **Kim G. Larsen**, **Axel Legay**, **Marius Mikučionis** and **Danny Bøgsted Poulsen**. In: _International Journal on Software Tools for Technology Transfer_ 17, 397–415 (2015). [doi:10.1007/s10009-014-0361-y](https://doi.org/10.1007/s10009-014-0361-y)
An extensive overview and comparison of methods for computing confidence intervals for binomial distribution can be found in the following publications:

> _Interval Estimators for a Binomial Proportion: Comparison of Twenty Methods_, **Ana M. Pires** and **Conceicao Amado**. REVSTAT -- Statistical Journal, Vol.6, No.2, June 2008, pages 165-197.
> _Interval Estimators for a Binomial Proportion: Comparison of Twenty Methods_, **Ana M. Pires** and **Conceicao Amado**. REVSTAT -- Statistical Journal, Vol.6, No.2, June 2008, pages 165-197. [doi:10.57805/revstat.v6i2.63](https://doi.org/10.57805/revstat.v6i2.63)
> _Interval Estimation for a Binomial Proportion_, **Lawrence D. Brown**, **T. Tony Cai** and **Anirban DasGupta**. Statistical Science, 2001, Vol.16, No.2, pages 101-133.
> _Interval Estimation for a Binomial Proportion_, **Lawrence D. Brown**, **T. Tony Cai** and **Anirban DasGupta**. Statistical Science, 2001, Vol.16, No.2, pages 101-133. [JSTOR](http://www.jstor.org/stable/2676784)

0 comments on commit ce1ebad

Please sign in to comment.