تعداد نشریات | 31 |
تعداد شمارهها | 508 |
تعداد مقالات | 4,931 |
تعداد مشاهده مقاله | 7,589,547 |
تعداد دریافت فایل اصل مقاله | 5,645,753 |
Upper bound of Policies for Statistical Model Checking of Markov Decision Processes | ||
Contributions of Science and Technology for Engineering | ||
مقالات آماده انتشار، پذیرفته شده، انتشار آنلاین از تاریخ 07 مهر 1404 | ||
نوع مقاله: Original Article | ||
شناسه دیجیتال (DOI): 10.22080/cste.2025.28924.1025 | ||
نویسنده | ||
Mohammadsadegh Mohagheghi* | ||
Vali-e-Asr University of Rafsanjan | ||
تاریخ دریافت: 14 فروردین 1404، تاریخ بازنگری: 10 مرداد 1404، تاریخ پذیرش: 07 مهر 1404 | ||
چکیده | ||
State explosion is a predominant challenge of model checking in all variants. Statistical model checking (SMC) is proposed to tackle this problem, which leads to promising results in most cases. Computing near-optimal policies for resolving non-deterministic choices is the main obstacle for applying SMC in the verification of Markov decision processes (MDPs). Although several solutions are available to cope with this problem they mainly suffer from memory limitation or non-accurate results with the given confidence level. In this paper, we define a criterion for the fitness of policies. We propose a novel method that provides an upper-bound for the number of policies needed to guarantee the precision of computed values with the desired level of confidence. The proposed criterion relies on statistical analysis on a set of randomly generated policies. It considers the mean and expected values of the computed reachability probabilities for the states of the model to determine an appropriate upper bound for the number of policies. We run a set of experiments for the proposed method. | ||
کلیدواژهها | ||
Formal Verification؛ Markov Decision Process؛ Statistical Model Checking؛ Confidence Interval | ||
آمار تعداد مشاهده مقاله: 0 |