| Class | Description |
|---|---|
| BlackboxApprox |
Vesta black-box approach by Sen et al.,
CAV 2004
"Statistical Model-checking of Black-box Probabilistic Systems Vesta"
th : threshold
|
| GenericApprox |
Generic approximation by Lassaigne et al.,
Ann.
|
| nGenericApprox |
Generic approximation by Lassaigne et al.,
Ann.
|
| OptimalApprox |
Optimal approximation by Dagum et al.,
SIAM Journal on Computing 2000
"An Optimal Algorithm for Monte Carlo Estimation"
0 < epsilon <= 1, 0 < delta <= 1, c > 1, z: property (0 means ip, 1 means tp)
UNFINISHED
|
| QAApprox |
Quantitative analysis by Kim et al.,
FMOODS 2007
"A Probabilistic Formal Approach to Cross-layer Optimization in Distributed Embedded Systems"
alpha: error bound, delta: confidence interval, pval: pvalue for JB test
minsize: minimum rounds, maxsize: maximum rounds, rate: % of sample (=rounds) increase
|
| SeqTestApprox |
Sequential probability ratio test by Younes et al.,
Journal on Software Tools for Technology Transfer 2006
"Numerical vs.
|
| Synchronize |