On the sequential massart algorithm for statistical model checking

Several schemes have been provided in Statistical Model Checking (SMC) for the estimation of property occurrence based on predefined confidence and absolute or relative error. Simulations might be however costly if many samples are required and the usual algorithms implemented in statistical model c...

وصف كامل

محفوظ في:
التفاصيل البيبلوغرافية
المؤلفون الرئيسيون: JEGOUREL, Cyrille, SUN, Jun, DONG, Jin Song
التنسيق: text
اللغة:English
منشور في: Institutional Knowledge at Singapore Management University 2018
الموضوعات:
الوصول للمادة أونلاين:https://ink.library.smu.edu.sg/sis_research/4653
https://ink.library.smu.edu.sg/context/sis_research/article/5656/viewcontent/ON_THE_SEQUENTIAL.pdf
الوسوم: إضافة وسم
لا توجد وسوم, كن أول من يضع وسما على هذه التسجيلة!
المؤسسة: Singapore Management University
اللغة: English
الوصف
الملخص:Several schemes have been provided in Statistical Model Checking (SMC) for the estimation of property occurrence based on predefined confidence and absolute or relative error. Simulations might be however costly if many samples are required and the usual algorithms implemented in statistical model checkers tend to be conservative. Bayesian and rare event techniques can be used to reduce the sample size but they can not be applied without prerequisite or knowledge about the system under scrutiny. Recently, sequential algorithms based on Monte Carlo estimations and Massart bounds have been proposed to reduce the sample size while providing guarantees on error bounds which has been shown to outperform alternative frequentist approaches [15]. In this work, we discuss some features regarding the distribution and the optimisationof these algorithms.