Notes:
The original publication is available at link.springer.com.
|
Links:
[Google]
[Google Scholar]
|
Abstract.
Numerical analysis based on uniformisation and statistical techniques
based on sampling and simulation are two distinct approaches for
transient analysis of stochastic systems. We compare the two solution
techniques when applied to the verification of time-bounded until
formulae in the temporal stochastic logic CSL, both theoretically and
through empirical evaluation on a set of case studies. Our study
differs from most previous comparisons of numerical and statistical
approaches in that CSL model checking is a hypothesis testing problem
rather than a parameter estimation problem. We can therefore rely on
highly efficient sequential acceptance sampling tests, which enables
statistical solution techniques to quickly return a result with some
uncertainty. We also propose a novel combination of the two solution
techniques for verifying CSL queries with nested probabilistic
operators.
|