Probabilistic verification of discrete event systems using acceptance sampling
Abstract
We propose a model independent procedure for verifying properties of
discrete event systems. The dynamics of such systems can be very
complex, making them hard to analyze, so we resort to methods based on
Monte Carlo simulation and statistical hypothesis testing. The
verification is probabilistic in two senses. First, the properties,
expressed as CSL formulas, can be probabilistic. Second, the result
of the verification is probabilistic, and the probability of error is
bounded by two parameters passed to the verification procedure. The
verification of properties can be carried out in an anytime manner by
starting off with loose error bounds, and gradually tightening these
bounds.
Sample citation
Håkan L. S. Younes and
Reid G. Simmons. 2002.
Probabilistic verification of discrete event systems using acceptance sampling. In
Proceedings of the 14th International Conference on Computer Aided Verification, edited by Ed Brinksma and Kim Guldstrand Larsen, vol. 2404 of
Lecture Notes in Computer Science, 223–235, Copenhagen, Denmark. Springer.
Full paper (13 pages, 16 references)
© Springer-Verlag 2002
Presentation (43 slides)